Sciweavers

ZUM
2000
Springer

Analysis of Compiled Code: A Prototype Formal Model

14 years 2 months ago
Analysis of Compiled Code: A Prototype Formal Model
Abstract. This paper reports on an experimental application of formal specification to inform analysis of compiled code. The analyses with are concerned attempt to recover abstraction and order from the potentially chaotic world of machine code. To illustrate the kind of abstractions of interest, we give a formal model of a simple microprocessor. This is based on a traditional state-based Z specification, but builds on that to produce a behavioural model of the microprocessor. We use the behavioural model to specify a higher-order notion: the concept of a program whose control flow can be decomposed into basic blocks. Finally, we report on the use of our techniques in the development of tools for analysis of compiled code for a real microprocessor.
R. D. Arthan
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 2000
Where ZUM
Authors R. D. Arthan
Comments (0)