Separation and information hiding

DOI10.1145/964001.964024zbMath1325.68069OpenAlexW2080769562MaRDI QIDQ3452266

John C. Reynolds, Hongseok Yang, Peter W. O'Hearn

Publication date: 11 November 2015

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

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

zbMATH Keywords

modularityseparation logicresource protection

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (31)

Program Verification with Separation Logic ⋮ Completeness for recursive procedures in separation logic ⋮ A First-Order Logic with Frames ⋮ Certifying low-level programs with hardware interrupts and preemptive threads ⋮ Bringing Order to the Separation Logic Jungle ⋮ Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Verifying pointer safety for programs with unknown calls ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ Exploring an Interface Model for CKA ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Safe Modification of Pointer Programs in Refinement Calculus ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Tackling Real-Life Relaxed Concurrency with FSL++ ⋮ Abstracting Complex Data Structures by Hyperedge Replacement ⋮ Hoare type theory, polymorphism and separation ⋮ Separation Logic for Multiple Inheritance ⋮ Weak updates and separation logic ⋮ The dynamic frames theory ⋮ Fifty years of Hoare's logic ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Secure the Clones ⋮ Verification of Equivalent-Results Methods ⋮ A shape graph logic and a shape system ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures ⋮ Parameterised notions of computation ⋮ Certificates and Separation Logic ⋮ Behaviour approximated on subgroups ⋮ Separation Logic Contracts for a Java-Like Language with Fork/Join ⋮ A proof outline logic for object-oriented programming

This page was built for publication: Separation and information hiding