A Formal Basis for a Program Compilation Proof Tool

Wildman, Luke (2002). A Formal Basis for a Program Compilation Proof Tool. In: L.-H. Eriksson and P. A. Lindsay, FME2002: Formal Methods - Getting IT Right. 11th International Symposium of Formal Methods Europe, Copenhagen, Denmark, (370-389). 22-24 July, 2002.


Author Wildman, Luke
Title of paper A Formal Basis for a Program Compilation Proof Tool
Conference Paper Type Fully Published Paper
Conference name 11th International Symposium of Formal Methods Europe
DOI 10.1007/3-540-45614-7_28
Conference location Copenhagen, Denmark
Conference dates 22-24 July, 2002
Proceedings title FME2002: Formal Methods - Getting IT Right
Editor L.-H. Eriksson
P. A. Lindsay
Place published Berlin
Publisher Springer
Publication date 2002
Volume number Lecture Notes in computer Science 2391
ISBN 978-3-540-43928-8
ISSN 0302-9743; 1611-3349
Start page 370
End page 389
Total pages 20
Collection year 2002
Language eng
Abstract/Summary This paper presents a case study in verified program compilation from high-level language programs to assembler code using the Cogito formal development system. A form of window-inference based on the Z schema is used to perform the compilation. Data-refinement is used to change the representation of integer variables to assembler word locations.
Subjects 280300 Computer Software
280302 Software Engineering
280000 Information, Computing and Communication Sciences
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Unknown

 
Versions
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 33 Abstract Views  -  Detailed Statistics
Created: Wed, 12 Apr 2006, 03:21:35 EST