Separation logic for small-step Cminor

Andrew W. Appel, Sandrine Blazy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

49 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationTheorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings
PublisherSpringer Verlag
Pages5-21
Number of pages17
ISBN (Print)9783540745907
DOIs
StatePublished - 2007
Event20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 - Kaiserslautern, Germany
Duration: Sep 10 2007Sep 13 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4732 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007
CountryGermany
CityKaiserslautern
Period9/10/079/13/07

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Separation logic for small-step Cminor'. Together they form a unique fingerprint.

  • Cite this

    Appel, A. W., & Blazy, S. (2007). Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings (pp. 5-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4732 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_3