Separation Logic for Non-local Control Flow and Block Scope Variables

DOI10.1007/978-3-642-37075-5_17zbMath1260.68101OpenAlexW2167148498MaRDI QIDQ4910424

Freek Wiedijk, Robbert Krebbers

Publication date: 18 March 2013

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

Full work available at URL: https://doi.org/10.1007/978-3-642-37075-5_17

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Aliasing Restrictions of C11 Formalized in Coq ⋮ A formal C memory model for separation logic ⋮ From specification to testing: semantics engineering for Lua 5.2

Uses Software

• Coq
• Isabelle
• CompCert
• cminor

This page was built for publication: Separation Logic for Non-local Control Flow and Block Scope Variables