This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First International Conference on Software Engineering and Formal Methods (SEFM'03)
A Partial-Correctness Semantics for Modelling Assembler Programs
Brisbane, Australia
September 22-September 27
ISBN: 0-7695-1949-0
ASCII Text
x 
 
Geoffrey Watson, Colin Fidge, "A Partial-Correctness Semantics for Modelling Assembler Programs," Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp. 82, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/SEFM.2003.1236210,
author = {Geoffrey Watson and Colin Fidge},
title = {A Partial-Correctness Semantics for Modelling Assembler Programs},
journal ={Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)},
volume = {0},
year = {2003},
isbn = {0-7695-1949-0},
pages = {82},
doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2003.1236210},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
TI - A Partial-Correctness Semantics for Modelling Assembler Programs
SN - 0-7695-1949-0
SP
EP
A1 - Geoffrey Watson,
A1 - Colin Fidge,
PY - 2003
KW - null
VL - 0
JA - Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
ER -
 
Geoffrey Watson, University of Queensland
Colin Fidge, University of Queensland

Previous work on formally modelling and analysing program compilation has shown the need for a simple and expressive semantics for assembler level programs.

Assembler programs contain unstructured jumps and previous formalisms have modelled these by using continuations, or by embedding the program in an explicit emulator. We propose a simpler approach, which uses techniques from compiler theory in a formal setting. This approach is based on an interpretation of programs as collections of program paths, each of which has a weakest liberal precondition semantics.

We then demonstrate, by example, how we can use this formalism to justify the compilation of block-structured high-level language programs into assembler.

Citation:
Geoffrey Watson, Colin Fidge, "A Partial-Correctness Semantics for Modelling Assembler Programs," sefm, pp.82, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.