The Relationship Between Separation Logic and Implicit Dynamic Frames

DOI10.2168/LMCS-8(3:1)2012zbMath1256.03036MaRDI QIDQ2904617

Alexander J. Summers, Matthew J. Parkinson

Publication date: 15 August 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

concurrencyseparation logicpermissionsfirst-order automatic verification tool Chaliceimplicit dynamic framespartial heapsverification logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (3)

Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Verification of Concurrent Systems with VerCors ⋮ Unifying separation logic and region logic to allow interoperability

Uses Software

• Dafny
• Boogie
• cminor

This page was built for publication: The Relationship Between Separation Logic and Implicit Dynamic Frames