This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Separation logic
A subject the papers are about. The loosest grouping, and the one to reach for last.
Reasoning about the heap when pointers may alias. Collects the logic itself, its BI foundations, and the decidability and automation results that follow -- including the separating implication, where most of the difficulty lives. Works the logic argues with, such as Girard's linear logic, belong here as antecedents rather than as members of the tradition.
112 references
Completeness of Iris-Based Program Logics
Johannes Hostert and others (2026) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery (ACM)
Separation Logic for Memory Conflict Detection in High-Level Synthesis
Yeonseok Lee (2026)
New Foundations for Separation Logic (Coq artifact)
Hans-Dieter Hiep (2024) · Zenodo
New Foundations for Separation Logic
Hans-Dieter A. Hiep (2024)
Dynamic Separation Logic
Frank S. de Boer and others (2023) · 39th Conference on the Mathematical Foundations of Programming Semantics (MFPS) · Electronic Notes in Theoretical Informatics and Computer Science
Foundations for entailment checking in quantitative separation logic
Kevin Batz and others (2022) · 31st European Symposium on Programming (ESOP) · Springer
Footprint Logic for Object-Oriented Components
Frank S. de Boer and others (2022) · Formal Aspects of Component Software · Springer International Publishing
Sound automation of magic wands
Thibault Dardinier and others (2022) · 34th International Conference on Computer Aided Verification (CAV) · Springer
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin and others (2022) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Strong-separation logic
Jens Pagel and others (2022) · ACM Transactions on Programming Languages and Systems (TOPLAS)
Permission-based verification of red-black trees and their merging
Lukas Armborst and others (2021) · 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE) · IEEE
A Complete Axiomatisation for Quantifier-Free Separation Logic
Stéphane Demri and others (2021) · Logical Methods in Computer Science · Logical Methods in Computer Science e.V.
Gobra: Modular specification and verification of Go programs
Felix A. Wolf and others (2021) · 33rd International Conference on Computer Aided Verification (CAV) · Springer
A probabilistic separation logic
Gilles Barthe and others (2020) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Separation logic for sequential programs (functional pearl)
Arthur Charguéraud (2020) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
Mnacho Echenim and others (2020) · ACM Transactions on Computational Logic (TOCL)
Dynamic Separation Logic and its Use in Education
Evgeny M. Makarov (2020) · Современные информационные технологии и ИТ-образование
A First-Order Logic with Frames
Adithya Murali and others (2020) · 29th European Symposium on Programming (ESOP) · Springer
Forward with separation logic
Callum Bannister (2019)
Separation logic
Peter W. O'Hearn (2019) · Communications of the ACM
Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation
Long H. Pham and others (2019) · Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings · Springer
Why Separation Logic Works
David Pym and others (2019) · Philosophy & Technology · Springer
SL-COMP: Competition of Solvers for Separation Logic
Mihaela Sighireanu and others (2019) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer
Backwards and Forwards with Separation Logic
Callum Bannister and others (2018) · 9th International Conference on Interactive Theorem Proving (ITP) · Springer
On models of higher-order separation logic
Aleš Bizjak and others (2018) · Electronic Notes in Theoretical Computer Science
The effects of adding reachability predicates in propositional separation logic
Stéphane Demri and others (2018) · 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) · Springer
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Mnacho Echenim and others (2018) · arXiv
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Ralf Jung and others (2018) · Journal of Functional Programming · Cambridge University Press
RustBelt: Securing the foundations of the Rust programming language
Ralf Jung and others (2018) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Biabduction (and Related Problems) in Array Separation Logic
James Brotherston and others (2017) · Automated Deduction – CADE 26 · Springer
Bringing order to the separation logic jungle
Qinxiang Cao and others (2017) · 15th Asian Symposium on Programming Languages and Systems (APLAS) · Springer
Interactive proofs in higher-order concurrent separation logic
Robbert Krebbers and others (2017) · 44th ACM Symposium on Principles of Programming Languages (POPL)
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Quang Loc Le and others (2017) · Computer Aided Verification · Springer
Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic
Andrew Reynolds and others (2017) · 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) · Springer
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Thomas Ströder and others (2017) · Journal of Automated Reasoning · Springer
Completeness for recursive procedures in separation logic
Mahmudul Faisal Al Ameen and others (2016) · Theoretical Computer Science · Elsevier
Completeness of Verification System with Separation Logic for Recursive Procedures
Mahmudul Faisal Al Ameen (2016) · The Graduate University for Advanced Studies, SOKENDAI
Concurrent separation logic
Stephen Brookes and others (2016) · ACM SIGLOG News
Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
Stéphane Demri and others (2016) · ACM Transactions on Computational Logic
Completeness for a first-order abstract separation logic
Zhé Hóu and others (2016) · 14th Asian Symposium on Programming Languages and Systems (APLAS) · Springer
Proof automation for functional correctness in separation logic
Ewen Maclean and others (2016) · Journal of Logic and Computation
Viper: A verification infrastructure for permission-based reasoning
Peter Müller and others (2016) · Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17 · Springer
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds and others (2016) · Automated Technology for Verification and Analysis · Springer
Permission-based separation logic for multithreaded Java programs
Afshin Amighi and others (2015) · Logical Methods in Computer Science
Witnessing the elimination of magic wands
Stefan Blom and others (2015) · International Journal on Software Tools for Technology Transfer · Springer
Being and Change: Reasoning About Invariance
Frank S. de Boer and others (2015) · Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings
Logical Investigations on Separation Logics
Stéphane Demri and others (2015) · 27th European Summer School in Logic, Language and Information (ESSLLI 2015)
Separation logics and modalities: a survey
Stéphane Demri and others (2015) · Journal of Applied Non-Classical Logics
A Program Construction and Verification Tool for Separation Logic
Brijesh Dongol and others (2015) · Mathematics of Program Construction · Springer
From categorical logic to Facebook engineering
Peter O'Hearn (2015) · 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science · IEEE
Foundations for Decision Problems in Separation Logic with General Inductive Predicates
Timos Antonopoulos and others (2014) · Foundations of Software Science and Computation Structures · Springer
A Decision Procedure for Satisfiability in Separation Logic with Inductive Definitions
James Brotherston and others (2014) · Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) · Association for Computing Machinery
A proof system for separation logic with magic wand
Wonyeol Lee and others (2014) · ACM SIGPLAN Notices · Association for Computing Machinery
Communicating state transition systems for fine-grained concurrent resources
Aleksandar Nanevski and others (2014) · 23rd European Symposium on Programming Languages and Systems (ESOP) · Springer
Automating Separation Logic with Trees and Data
Ruzica Piskac and others (2014) · Computer Aided Verification · Springer
Completeness of separation logic with inductive definitions for program verification
Makoto Tatsuta and others (2014) · International Conference on Software Engineering and Formal Methods · Springer
Satisfiability modulo abstraction for separation logic with linked lists
Aditya Thakur and others (2014) · International SPIN Symposium on Model Checking of Software · Association for Computing Machinery
A Simple Separation Logic
Andreas Herzig (2013) · Logic, Language, Information, and Computation · Springer
The Tree Width of Separation Logic with Recursive Definitions
Radu Iosif and others (2013) · Automated Deduction – CADE-24 · Springer
Automating Separation Logic Using SMT
Ruzica Piskac and others (2013) · Computer Aided Verification · Springer
Separation predicates: A taste of separation logic in first-order logic
François Bobot and others (2012) · International Conference on Formal Engineering Methods · Springer
On the almighty wand
Rémi Brochenin and others (2012) · Information and Computation
A Primer on Separation Logic (and Automatic Program Verification and Analysis)
Peter W. O'Hearn (2012) · Software Safety and Security: Tools for Analysis and Verification · IOS Press
Compositional Shape Analysis by Means of Bi-Abduction
Cristiano Calcagno and others (2011) · Journal of the ACM · Association for Computing Machinery
Mostly-automated verification of low-level programs in computational separation logic
Adam Chlipala (2011) · 32nd ACM Conference on Programming Language Design and Implementation (PLDI)
Algebraic separation logic
Han Hing Dang and others (2011) · The Journal of Logic and Algebraic Programming · Elsevier
Verification of programs in virtual memory using separation logic
Rafal Michal Kolanski (2011) · UNSW Sydney
Undecidability of propositional separation logic and its neighbours
James Brotherston and others (2010) · 25th IEEE Symposium on Logic in Computer Science (LICS) · IEEE
Tableaux and resource graphs for separation logic
Didier Galmiche and others (2010) · Journal of Logic and Computation
Design patterns in separation logic
Neelakantan R. Krishnaswami and others (2009) · 4th International Workshop on Types in Language Design and Implementation · Association for Computing Machinery
A Certified Verifier for a Fragment of Separation Logic
Nicolas Marti and others (2009) · Information and Media Technologies
An Introduction to Separation Logic
John C. Reynolds (2009) · Engineering Methods and Tools for Software Safety and Security · IOS Press
Completeness of Pointer Program Verification by Separation Logic
Makoto Tatsuta and others (2009) · 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods · IEEE
Cyclic proofs of program termination in separation logic
James Brotherston and others (2008) · ACM SIGPLAN Notices
jStar: Towards Practical Verification for Java
Dino Distefano and others (2008) · Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications · Association for Computing Machinery
A Modal Sequent Calculus for Propositional Separation Logic
Neelakantan R. Krishnaswami (2008) · IMLA 2008: 4th Workshop on Intuitionistic Modal Logic and Applications
An Overview of Separation Logic
John Reynolds (2008) · Verified Software: Theories, Tools, Experiments · Springer
Relational parametricity and separation logic
Lars Birkedal and others (2007) · 10th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS) · Springer
A semantics for concurrent separation logic
Stephen Brookes (2007) · Theoretical Computer Science · Elsevier
Local reasoning about data update
Cristiano Calcagno and others (2007) · Electronic Notes in Theoretical Computer Science
Local Action and Abstract Separation Logic
Cristiano Calcagno and others (2007) · 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) · IEEE
Resources, concurrency, and local reasoning
Peter W. O'Hearn (2007) · Theoretical Computer Science · Elsevier
Types, bytes, and separation logic
Harvey Tuch and others (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)
Smallfoot: Modular Automatic Assertion Checking with Separation Logic
Josh Berdine and others (2006) · Formal Methods for Components and Objects · Springer Berlin Heidelberg
A Local Shape Analysis Based on Separation Logic
Dino Distefano and others (2006) · Tools and Algorithms for the Construction and Analysis of Systems · Springer
Expressivity properties of Boolean BI through relational models
Didier Galmiche and others (2006) · 26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) · Springer
Verifying properties of well-founded linked lists
Shuvendu K. Lahiri and others (2006) · ACM SIGPLAN Notices · Association for Computing Machinery
Separation logic for higher-order store
Bernhard Reus and others (2006) · 20th International Workshop on Computer Science Logic (CSL) · Springer
Symbolic Execution with Separation Logic
Josh Berdine and others (2005) · Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings · Springer
Permission accounting in separation logic
Richard Bornat and others (2005) · Proceedings of the 32nd ACM Symposium on Principles of Programming Languages
From separation logic to first-order logic
Cristiano Calcagno and others (2005) · 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS) · Springer
A Decidable Fragment of Separation Logic
Josh Berdine and others (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science · Springer
Generalized Records and Spatial Conjunction in Role Logic
Viktor Kuncak and others (2004) · Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings · Springer
On Spatial Conjunction as Second-Order Logic
Viktor Kuncak and others (2004) · arXiv
Extending Separation Logic with Fixpoints and Postponed Substitution
Élodie-Jane Sims (2004) · Algebraic Methodology and Software Technology · Springer
Towards mechanized program verification with separation logic
Tjark Weber (2004) · 18th International Workshop on Computer Science Logic (CSL) · Springer
A proof system for object oriented programming using separation logic
Ronald Middelkoop (2003) · Technische Universiteit Eindhoven
Semantic and Logical Properties of Stateful Programming
Cristiano Calcagno (2002) · Universita di Genova
The Semantics and Proof Theory of the Logic of Bunched Implications
David J. Pym (2002) · Springer
Separation logic: a logic for shared mutable data structures
John C. Reynolds (2002) · Proceedings 17th Annual IEEE Symposium on Logic in Computer Science · IEEE
A Semantic Basis for Local Reasoning
Hongseok Yang and others (2002) · Foundations of Software Science and Computation Structures · Springer
Computability and Complexity Results for a Spatial Assertion Language for Data Structures
Cristiano Calcagno and others (2001) · Foundations of Software Technology and Theoretical Computer Science (FSTTCS) · Springer
BI as an assertion language for mutable data structures
Samin S. Ishtiaq and others (2001) · 28th ACM Symposium on Principles of Programming Languages (POPL)
Local Reasoning about Programs that Alter Data Structures
Peter W. O'Hearn and others (2001) · Computer Science Logic · Springer
Local reasoning for stateful programs
Hongseok Yang (2001) · University of Illinois
Proving pointer programs in Hoare logic
Richard Bornat (2000) · 5th International Conference on Mathematics of Program Construction (MPC) · Springer
Intuitionistic Reasoning about Shared Mutable Data Structure
John C. Reynolds (2000) · Millennial Perspectives in Computer Science · Macmillan Education UK
The logic of bunched implications
Peter W. O'Hearn and others (1999) · Bulletin of Symbolic Logic
Static detection of pointer errors: an axiomatisation and a checking algorithm
Pascal Fradet and others (1996) · European Symposium on Programming · Springer
Linear logic
Jean-Yves Girard (1987) · Theoretical Computer Science · Elsevier BV
Proving assertions about programs that manipulate data structures
Derek C. Oppen and others (1975) · 7th ACM Symposium on Theory of Computing
Some techniques for proving correctness of programs which alter data structures
Rodney M. Burstall (1972) · Machine intelligence