Paper Info
Title
Mechanized operational semantics of WSL
Abstract
This paper presents an experiment on computer assisted formal verification of program transformations. The operational semantics of WSL is formalized in the type theoretical proof assistant Coq, which forms the basis on which the correctness of program transformations can be stated and proved as formulae in Coq. A group of program transformations frequently used for software maintenance have been proved correct. The existence of a machine checked formal verification increases significantly the confidence in the correctness of program transformations, which is crucial for the reliability of software maintenance systems.
Year
DOI
Venue
2002
10.1109/SCAM.2002.1134107
SCAM
Keywords
Field
DocType
coq type theoretical proof assistant,wsl,machine checked formal verification,programming language semantics,software maintenance,integral part,computer assisted formal verification,programming language meta-model,reliability,complexity metrics,program transformation correctness,existing production-quality compiler,program verification,mechanized operational semantics,computer languages,mathematics,computer science,proof assistant,formal verification,operational semantics
Operational semantics,Programming language,Program transformation,Computer science,Constraint theory,Correctness,Theoretical computer science,Software maintenance,Program analysis,Formal verification,Proof assistant
Conference
ISBN
Citations 
PageRank 
0-7695-1793-5
6
0.43
References 
Authors
5
4
Name
Order
Citations
PageRank
xingyuan zhang11069.80
Malcolm Munro2877199.56
Mark Harman310264389.82
Lin Hu41469.44