Separation logic and abstraction
From MaRDI portal
Publication:5276150
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
Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
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
