Separation logic, abstraction and inheritance

DOI10.1145/1328438.1328451zbMath1295.68091MaRDI QIDQ3189828

G. M. Bierman, Matthew J. Parkinson

Publication date: 12 September 2014

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

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

zbMATH Keywords

modularity; separation logic

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

68N15: Theory of programming languages

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

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

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Separation Logic for Multiple Inheritance, Higher-Order Separation Logic in Isabelle/HOLCF, Separation Logic Contracts for a Java-Like Language with Fork/Join, Incremental reasoning with lazy behavioral subtyping for multiple inheritance, Lazy behavioral subtyping, Verifying traits: an incremental proof system for fine-grained reuse, Automatic verification of Java programs with dynamic frames, Unifying separation logic and region logic to allow interoperability, Verified software units, Certificates and Separation Logic, Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq, Specification Patterns and Proofs for Recursion through the Store, WP Semantics and Behavioral Subtyping, Undecidability of Propositional Separation Logic and Its Neighbours, Incremental Reasoning for Multiple Inheritance, Nested Hoare Triples and Frame Rules for Higher-Order Store