Sciweavers

Share
TACAS
2007
Springer

Hoare Logic for Realistically Modelled Machine Code

12 years 3 months ago
Hoare Logic for Realistically Modelled Machine Code
This paper presents a mechanised Hoare-style programming logic framework for assembly level programs. The framework has been designed to fit on top of operational semantics of realistically modelled machine code. Many ad hoc restrictions and features present in real machine-code are handled, including finite memory, data and code in the same memory space, the behavior of status registers and hazards of corrupting special purpose registers (e.g. the program counter, procedure return register and stack pointer). Despite accurately modeling such low level details, the approach yields concise specifications for machinecode programs without using common simplifying assumptions (like an unbounded state space). The framework is based on a flexible state representation in which functional and resource usage specifications are written in a style inspired by separation logic. The presented work has been formalised in higher-order logic, mechanised in the HOL4 system and is currently being u...
Magnus O. Myreen, Michael J. C. Gordon
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TACAS
Authors Magnus O. Myreen, Michael J. C. Gordon
Comments (0)
books