Separation Logic for Small-Step cminor. 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.

References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Krebbers, Robbert: An operational and axiomatic semantics for non-determinism and sequence points in C (2014)
  2. Krebbers, Robbert; Wiedijk, Freek: Separation logic for non-local control flow and block scope variables (2013)
  3. Leroy, Xavier: Mechanized semantics for compiler verification (2012)
  4. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2012)
  5. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)
  6. Leroy, Xavier: A formally verified compiler back-end (2009)
  7. McCreight, Andrew: Practical tactics for separation logic (2009)
  8. Tuch, Harvey: Formal verification of C systems code. Structured types, separation logic and theorem proving (2009)
  9. Dockins, Robert; Appel, Andrew W.; Hobor, Aquinas: Multimodal separation logic for reasoning about operational semantics (2008)
  10. Haack, Christian; Hurlin, Clément: Separation logic contracts for a Java-like language with fork/join (2008)
  11. Hobor, Aquinas; Appel, Andrew W.; Nardelli, Francesco Zappa: Oracle semantics for concurrent separation logic (2008)
  12. Leroy, Xavier; Blazy, Sandrine: Formal verification of a C-like memory model and its uses for verifying program transformations (2008)
  13. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step cminor (2007)
  14. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step Cminor (2007)