Separation logic for small-step cminor
作者： Andrew W. Appel , Sandrine Blazy
DOI: 10.1007/978-3-540-74591-4_3
关键词:
摘要: Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to and machine language. We have redesigned so that it suitable for Hoare Logic reasoning we designed Separation Cminor. In this paper, give small-step semantics (instead of the big-step compiler) motivated by need support future concurrent extensions. detail machine-checked proof soundness our Logic. This first large-scale w.r.t. semantics. The work presented in paper has been carried out Coq assistant. It step towards an environment which programs can be verified using also compiled compiler with formal end-to-end correctness guarantees.
springer.com
princeton.edu 
ensiie.fr 
irisa.fr 参考文章(17)
Norbert Schirmer, Verification of Sequential Imperative Programs in Isabelle/HOL pp. 1- 249 ,(2006)
Peter O’Hearn, John Reynolds, Hongseok Yang, Local Reasoning about Programs that Alter Data Structures computer science logic. ,vol. 2142, pp. 1- 19 ,(2001) , 10.1007/3-540-44802-0_1
Sandrine Blazy, Xavier Leroy, Formal verification of a memory model for C -like imperative languages formal methods. ,vol. 3785, pp. 280- 299 ,(2005) , 10.1007/11576280_20
Sandrine Blazy, Zaynah Dargaye, Xavier Leroy, Formal Verification of a C Compiler Front-End FM 2006: Formal Methods. ,vol. 4085, pp. 460- 475 ,(2006) , 10.1007/11813040_31
Norbert Schirmer, A verification environment for sequential imperative programs in isabelle/HOL international conference on logic programming. pp. 398- 414 ,(2005) , 10.1007/978-3-540-32275-7_26
Samin Ishtiaq, Peter W. O'Hearn, BI as an assertion language for mutable data structures ACM SIGPLAN Notices. ,vol. 46, pp. 84- 96 ,(2011) , 10.1145/1988042.1988050
Richard Bornat, Cristiano Calcagno, Peter O'Hearn, Matthew Parkinson, Permission accounting in separation logic symposium on principles of programming languages. ,vol. 40, pp. 259- 270 ,(2005) , 10.1145/1040305.1040327
JStrother Moore, A mechanically verified language implementation Journal of Automated Reasoning. ,vol. 5, pp. 461- 492 ,(1989) , 10.1007/BF00243133
Stephen Brookes, A Grainless Semantics for Parallel Programs with Shared Mutable Data Electronic Notes in Theoretical Computer Science. ,vol. 155, pp. 277- 307 ,(2006) , 10.1016/J.ENTCS.2005.11.060
Reynald Aeldt, Nicolas Marti, Towards Formal Verication of Memory Properties using Separation Logic ,(2005)