We introduce a Floyd-Hoare-style framework for specification and verification of machine code programs, based on relational parametricity (rather than unary predicates) and using both step-indexing and a novel form of separation structure. This yields compositional, descriptive and extensional reasoning principles for many features of low-level sequential computation: independence, ownership transfer, unstructured control flow, first-class code pointers and address arithmetic. We demonstrate how to specify and verify the implementation of a simple memory manager and, independently, its clients in this style. The work has been fully machine-checked within the Coq proof assistant. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Benton, N. (2006). Abstracting allocation: The new new thing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4207 LNCS, pp. 182–196). Springer Verlag. https://doi.org/10.1007/11874683_12
Mendeley helps you to discover research relevant for your work.