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
Reports

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 :
Reports
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/inria-00134699
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

sequential-rr.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00134699, version 5

Collections

Citation

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

Share

Metrics

Record views

322

Files downloads

382