Separation Logic Tutorial

DOI10.1007/978-3-540-89982-2_6MaRDI QIDQ5504642zbMATH OpenOpenAlexFDO

Authors Peter W. O'Hearn

Publication date 22 January 2009

Published in Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89982-2_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Separation Logic for Higher-Order Store
• Separation logic and concurrency
• Fictional separation logic
• Program Verification with Separation Logic
• Computer Science Logic

Cites work

• A semantics for concurrent separation logic
• A semantics for procedure local heaps and its abstractions
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Enhancing Program Verification with Lemmas
• Hoare Logic for Realistically Modelled Machine Code
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Scalable Shape Analysis for Systems Code
• Separation logic and abstraction
• Shape Analysis for Composite Data Structures
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• Tools and Algorithms for the Construction and Analysis of Systems
• Types, bytes, and separation logic

Cited in

(8)

• Backwards and forwards with separation logic
• Fictional separation logic
• Relational Parametricity and Separation Logic
• Separation logics and modalities: a survey
• A proof system for separation logic with magic wand
• Relational Parametricity and Separation Logic
• Separation logic style reasoning in a refinement based language
• Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Describes a project that uses

Uses Software

• jStar
• THOR
• Smallfoot

This page was built for publication: Separation Logic Tutorial

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5504642)