Separation logic and abstraction

DOI10.1145/1040305.1040326zbMath1369.68151OpenAlexW2171685273MaRDI QIDQ5276150

G. M. Bierman, Matthew J. Parkinson

Publication date: 14 July 2017

Published in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1040305.1040326

zbMATH Keywords

modularityresourcesseparation logicabstract data types

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (30)

Local Reasoning for Global Graph Properties ⋮ A First-Order Logic with Frames ⋮ Automatic Inference of Access Permissions ⋮ Caper ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ A perspective on specifying and verifying concurrent modules ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Blaming the client: on data refinement in the presence of pointers ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Unnamed Item ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Refactoring and representation independence for class hierarchies ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Verified software units ⋮ Separation Logic for Multiple Inheritance ⋮ The dynamic frames theory ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ Verification of Concurrent Systems with VerCors ⋮ Dynamic Frames in Java Dynamic Logic ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Verification of Equivalent-Results Methods ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ Graph-Based Object-Oriented Hoare Logic ⋮ Separation Logic Tutorial ⋮ Separation Logic Contracts for a Java-Like Language with Fork/Join ⋮ Invariants for Non-Hierarchical Object Structures

This page was built for publication: Separation logic and abstraction