Separation Logic Tutorial

DOI10.1007/978-3-540-89982-2_6zbMath1185.68228OpenAlexW2138403792MaRDI QIDQ5504642

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) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Uses Software

• Smallfoot
• jStar
• THOR

Cites Work

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

This page was built for publication: Separation Logic Tutorial