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