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
Conference papers

Separation Logic for Small-step Cminor

Abstract : Cminor is a mid-level imperative programming language; there are 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 and we have designed a Separation Logic for Cminor. In this paper, we give a small-step semantics (instead of the big-step of the proved-correct compiler) that is motivated by the need to support future concurrent extensions. We detail 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. The work presented in this paper has been carried out in the Coq proof assistant. It is a first step towards an environment in which concurrent Cminor programs can be verified using Separation Logic and also compiled by a proved-correct compiler with formal end-to-end correctness guarantees.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00165915
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Monday, July 30, 2007 - 2:02:06 PM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
Long-term archiving on: : Friday, April 9, 2010 - 12:12:10 AM

Files

paperTPHOL.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00165915, version 1
  • ARXIV : 0707.4389

Collections

Citation

Andrew W. Appel, Sandrine Blazy. Separation Logic for Small-step Cminor. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21. ⟨inria-00165915⟩

Share

Metrics

Record views

131

Files downloads

173