Separation Logic for Small-Step cminor

DOI10.1007/978-3-540-74591-4_3zbMath1144.68351arXiv0707.4389OpenAlexW1545100927MaRDI QIDQ3523161

Andrew W. Appel, Sandrine Blazy

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0707.4389

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Formal verification of C systems code. Structured types, separation logic and theorem proving, Practical Tactics for Separation Logic, A Formalisation of Smallfoot in HOL, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Lightweight Separation, Barriers in Concurrent Separation Logic, The Relationship between Separation Logic and Implicit Dynamic Frames, Formal verification of a C-like memory model and its uses for verifying program transformations, Proving correctness of a compiler using step-indexed logical relations, Multimodal Separation Logic for Reasoning About Operational Semantics, cminor, A Machine-Checked Framework for Relational Separation Logic

Uses Software

• Coq