loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Second IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'02)
Mechanized Operational Semantics of WSL
Montreal, Canada
October 01-October 01
ISBN: 0-7695-1793-5
ASCII Text
x 
 
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu, "Mechanized Operational Semantics of WSL," Source Code Analysis and Manipulation, IEEE International Workshop on, pp. 73, Second IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/SCAM.2002.1134107,
author = {Xingyuan Zhang and Malcolm Munro and Mark Harman and Lin Hu},
title = {Mechanized Operational Semantics of WSL},
journal ={Source Code Analysis and Manipulation, IEEE International Workshop on},
volume = {0},
year = {2002},
isbn = {0-7695-1793-5},
pages = {73},
doi = {http://doi.ieeecomputersociety.org/10.1109/SCAM.2002.1134107},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Source Code Analysis and Manipulation, IEEE International Workshop on
TI - Mechanized Operational Semantics of WSL
SN - 0-7695-1793-5
SP
EP
A1 - Xingyuan Zhang,
A1 - Malcolm Munro,
A1 - Mark Harman,
A1 - Lin Hu,
PY - 2002
KW - Program Transformation
KW - Computer Assisted Formal Reasoning
VL - 0
JA - Source Code Analysis and Manipulation, IEEE International Workshop on
ER -
 
Xingyuan Zhang, University of Durham
Malcolm Munro, University of Durham
Mark Harman, Brunel University
Lin Hu, Brunel University
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," scam, pp.73, Second IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.