HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Separation Logic for Small-step Cminor (extended version)

Abstract : Cminor is a mid-level imperative programming language (just below C), and there exist proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor so that it is suitable for Hoare Logic reasoning, we have designed a Separation Logic for Cminor, we have given a small-step operational semantics so that extensions to concurrent Cminor will be possible, and we have a machine-checked proof of soundness of our Separation Logic. This is the first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics, or for a language with nontrivial reducible control-flow constructs. Our sequential soundness proof of the sequential Separation Logic for the sequential language features will be reusable change within a soundness proof of Concurrent Separation Logic w.r.t. Concurrent Cminor. In addition, we have a machine-checked proof of the relation between our small-step semantics and Leroy's original big-step semantics; thus sequential programs can be compiled by Leroy's compiler with formal end-to-end correctness guarantees.
Document type :
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Thursday, August 30, 2007 - 3:38:32 PM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
Long-term archiving on: : Friday, September 24, 2010 - 12:06:29 PM


Files produced by the author(s)


  • HAL Id : inria-00134699, version 5



Andrew W. Appel, Sandrine Blazy. Separation Logic for Small-step Cminor (extended version). [Research Report] RR-6138, INRIA. 2007, pp.34. ⟨inria-00134699v5⟩



Record views


Files downloads