Unifying separation logic and region logic to allow interoperability
DOI10.1007/s00165-018-0455-5zbMath1398.68091OpenAlexW2803344012WikidataQ129769039 ScholiaQ129769039MaRDI QIDQ1798668
Gidon Ernst, Yuyan Bao, Gary T. Leavens
Publication date: 23 October 2018
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-018-0455-5
formal verificationformal specificationHoare logicseparation logicframingfine-grained region logicshared mutable dataunified fine-grained region logic (UFRL)
Logic in computer science (03B70) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The dynamic frames theory
- Automatic verification of Java programs with dynamic frames
- Modular invariants for layered object structures
- Decision Procedures for Region Logic
- The Relationship Between Separation Logic and Implicit Dynamic Frames
- The ramifications of sharing in data structures
- Dafny: An Automatic Program Verifier for Functional Correctness
- Tractable Reasoning in a Fragment of Separation Logic
- Separation logic, abstraction and inheritance
- Separation and information hiding
- Formalised Inductive Reasoning in the Logic of Bunched Implications
- A Basis for Verifying Multi-threaded Programs
- BI as an assertion language for mutable data structures
- Separation logic and abstraction
- Local Reasoning for Global Invariants, Part I
- Local Reasoning for Global Invariants, Part II
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Programming Languages and Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Modular specification and verification of object-oriented programs
This page was built for publication: Unifying separation logic and region logic to allow interoperability
