|
 
|
[AB07] Separation logic for small-step Cminor (extended version)
Rapport Scientifique : Date de dépot: 2007/01/01, Nb pages 29 pages, (Tech. Rep.: CEDRIC-07-1358)
motcle:
Résumé:
minor is a mid-level imperative programming language (just below C), and there exist 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, we have designed a Separation Logic for Cminor, we have given a small-step operational semantics so that extensions to concurrent Cminor will be possible, and we have 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, or for a language with nontrivial reducible control-flow constructs. Our sequential soundness proof of the sequential Separation Logic for the sequential language features will be reusable change within a soundness proof of Concurrent Separation Logic w.r.t. Concurrent Cminor. In addition, we have a machine-checked proof of the relation between our small-step semantics and Leroy's original big-step semantics; thus sequential programs can be compiled by Leroy's compiler with formal end-to-end correctness guarantees.
BibTeX
| @techreport { | |||
| AB07, | |||
| title | = | "{Separation logic for small-step Cminor (extended version)}", | |
| author | = | "A. Appel and S. Blazy", | |
| number | = | "{CEDRIC-07-1358}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-01-2007}, | |
| pages | = | "29 pages", | |
| } | |||
