The Community for Technology Leaders
2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM) (2002)
Montreal, Canada
Oct. 1, 2002 to Oct. 1, 2002
ISBN: 0-7695-1793-5
pp: 73
Xingyuan Zhang , University of Durham
Malcolm Munro , University of Durham
Mark Harman , Brunel University
Lin Hu , Brunel University
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 formul? 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.
INDEX TERMS
Program Transformation, Computer Assisted Formal Reasoning
CITATION
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu, "Mechanized Operational Semantics of WSL", 2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM), vol. 00, no. , pp. 73, 2002, doi:10.1109/SCAM.2002.1134107
99 ms
(Ver 3.1 (10032016))