The Relationship between Separation Logic and Implicit Dynamic Frames

DOI10.1007/978-3-642-19718-5_23zbMath1326.68104arXiv1203.6859OpenAlexW1522925810MaRDI QIDQ3000593

Matthew J. Parkinson, Alexander J. Summers

Publication date: 19 May 2011

Published in: Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A First-Order Logic with Frames ⋮ Bringing Order to the Separation Logic Jungle ⋮ Generalized arrays for Stainless frames ⋮ WP Semantics and Behavioral Subtyping ⋮ Verifying Whiley programs with Boogie

Uses Software

• Dafny
• Boogie
• cminor

Cites Work

• Unnamed Item
• Unnamed Item
• Dafny: An Automatic Program Verifier for Functional Correctness
• Separation Logic for Small-Step cminor
• A Basis for Verifying Multi-threaded Programs
• BI as an assertion language for mutable data structures
• Permission accounting in separation logic