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

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

  1. Rodríguez, Leonardo; Pagano, Miguel; Fridlender, Daniel: Proving correctness of a compiler using step-indexed logical relations (2016)
  2. Krebbers, Robbert: An operational and axiomatic semantics for non-determinism and sequence points in C (2014)
  3. Krebbers, Robbert; Wiedijk, Freek: Separation logic for non-local control flow and block scope variables (2013)
  4. Leroy, Xavier: Mechanized semantics for compiler verification (2012) ioport
  5. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2012)
  6. Crespo, Juan Manuel; Kunz, César: A machine-checked framework for relational separation logic (2011)
  7. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2011)
  8. McCreight, Andrew; Chevalier, Tim; Tolmach, Andrew: A certified framework for compiling and executing garbage-collected languages (2010)
  9. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)
  10. Leroy, Xavier: A formally verified compiler back-end (2009)
  11. McCreight, Andrew: Practical tactics for separation logic (2009)
  12. Tuch, Harvey: Formal verification of C systems code. Structured types, separation logic and theorem proving (2009)
  13. Tuerk, Thomas: A formalisation of Smallfoot in HOL (2009)
  14. Dockins, Robert; Appel, Andrew W.; Hobor, Aquinas: Multimodal separation logic for reasoning about operational semantics (2008)
  15. Haack, Christian; Hurlin, Clément: Separation logic contracts for a Java-like language with fork/join (2008)
  16. Hobor, Aquinas; Appel, Andrew W.; Nardelli, Francesco Zappa: Oracle semantics for concurrent separation logic (2008)
  17. Leroy, Xavier; Blazy, Sandrine: Formal verification of a C-like memory model and its uses for verifying program transformations (2008)
  18. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step cminor (2007) ioport
  19. Appel, Andrew W.; Blazy, Sandrine: Separation logic for small-step Cminor (2007)