cminor
swMATH ID:  9739 
Software Authors:  Appel, A.W., Blazy, S. 
Description:  Separation Logic for SmallStep cminor. cminor is a midlevel imperative programming language; there are provedcorrect 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 smallstep semantics (instead of the bigstep of the provedcorrect compiler) that is motivated by the need to support future concurrent extensions. We detail a machinechecked proof of soundness of our Separation Logic. This is the first largescale machinechecked proof of a Separation Logic w.r.t. a smallstep 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 provedcorrect compiler with formal endtoend correctness guarantees. 
Homepage:  http://link.springer.com/chapter/10.1007/9783540745914_3 
Related Software:  Coq; CompCert; Isabelle/HOL; CIL; Boogie; Dafny; veriSoft; Smallfoot; OCaml; MLCompCert; GCminor; GHC; Haskell; PoplMark; CompCertTSO; Isabelle; VeriFast; VLISP; TALx86; Piton 
Cited in:  17 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

Separation logic for smallstep Cminor. Zbl 1144.68351 Appel, Andrew W.; Blazy, Sandrine 
2007

all
top 5
Cited by 22 Authors
Cited in 2 Serials
4  Journal of Automated Reasoning 
1  Logical Methods in Computer Science 
Cited in 2 Fields
17  Computer science (68XX) 
9  Mathematical logic and foundations (03XX) 