The Relationship Between Separation Logic and Implicit Dynamic Frames

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

Matthew J. Parkinson, Alexander J. Summers

Publication date: 15 August 2012

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

zbMATH Keywords

concurrency; separation logic; permissions; first-order automatic verification tool Chalice; implicit dynamic frames; partial heaps; verification logics

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Uses Software

• Dafny
• Boogie
• cminor