cminor

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 18 articles , 1 standard article )

Showing results 1 to 18 of 18.
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) ioport
  4. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2012)
  5. Crespo, Juan Manuel; Kunz, César: A machine-checked framework for relational separation logic (2011)
  6. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2011)
  7. McCreight, Andrew; Chevalier, Tim; Tolmach, Andrew: A certified framework for compiling and executing garbage-collected languages (2010)
  8. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)
  9. Leroy, Xavier: A formally verified compiler back-end (2009)
  10. McCreight, Andrew: Practical tactics for separation logic (2009)
  11. Tuch, Harvey: Formal verification of C systems code. Structured types, separation logic and theorem proving (2009)
  12. Tuerk, Thomas: A formalisation of Smallfoot in HOL (2009)
  13. Dockins, Robert; Appel, Andrew W.; Hobor, Aquinas: Multimodal separation logic for reasoning about operational semantics (2008)
  14. Haack, Christian; Hurlin, Clément: Separation logic contracts for a Java-like language with fork/join (2008)
  15. Hobor, Aquinas; Appel, Andrew W.; Nardelli, Francesco Zappa: Oracle semantics for concurrent separation logic (2008)
  16. Leroy, Xavier; Blazy, Sandrine: Formal verification of a C-like memory model and its uses for verifying program transformations (2008)
  17. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step cminor (2007) ioport
  18. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step Cminor (2007)