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. Usually described as being about one connective; BI supplies two, and the second — the separating implication — is where the difficulty of deciding and automating it lives.
102 references
New Foundations for Separation Logic
Hans-Dieter A. Hiep (2024)
Dynamic Separation Logic
Frank S. de Boer et al. (2023) · 39th Conference on the Mathematical Foundations of Programming Semantics (MFPS)
Foundations for entailment checking in quantitative separation logic
Kevin Batz et al. (2022) · 31st European Symposium on Programming (ESOP)
Sound automation of magic wands
Thibault Dardinier et al. (2022) · 34th International Conference on Computer Aided Verification (CAV)
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin et al. (2022) · Proceedings of the ACM on Programming Languages
Strong-separation logic
Jens Pagel et al. (2022) · ACM Transactions on Programming Languages and Systems (TOPLAS)
Permission-based verification of red-black trees and their merging
Lukas Armborst et al. (2021) · 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE)
A Complete Axiomatisation for Quantifier-Free Separation Logic
Stéphane Demri et al. (2021) · Logical Methods in Computer Science
Gobra: Modular specification and verification of Go programs
Felix A. Wolf et al. (2021) · 33rd International Conference on Computer Aided Verification (CAV)
A probabilistic separation logic
Gilles Barthe et al. (2020) · Proceedings of the ACM on Programming Languages
Separation logic for sequential programs (functional pearl)
Arthur Charguéraud (2020) · Proceedings of the ACM on Programming Languages
The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
Mnacho Echenim et al. (2020) · ACM Transactions on Computational Logic (TOCL)
Dynamic Separation Logic and its Use in Education
Makarov Evgeny Maratovich (2020) · Современные информационные технологии и ИТ-образование
A First-Order Logic with Frames
Adithya Murali et al. (2020) · 29th European Symposium on Programming (ESOP)
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 et al. (2019) · Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
Why Separation Logic Works
David Pym et al. (2019) · Philosophy & Technology
SL-COMP: competition of solvers for separation logic
Mihaela Sighireanu et al. (2019) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Backwards and Forwards with Separation Logic
Callum Bannister et al. (2018) · 9th International Conference on Interactive Theorem Proving (ITP)
On models of higher-order separation logic
Aleš Bizjak et al. (2018) · Electronic Notes in Theoretical Computer Science
The effects of adding reachability predicates in propositional separation logic
Stéphane Demri et al. (2018) · 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Mnacho Echenim et al. (2018)
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Ralf Jung et al. (2018) · Journal of Functional Programming
Biabduction (and Related Problems) in Array Separation Logic
James Brotherston et al. (2017) · Automated Deduction – CADE 26
Bringing order to the separation logic jungle
Qinxiang Cao et al. (2017) · 15th Asian Symposium on Programming Languages and Systems (APLAS)
Interactive proofs in higher-order concurrent separation logic
Robbert Krebbers et al. (2017) · 44th ACM Symposium on Principles of Programming Languages (POPL)
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Quang Loc Le et al. (2017) · Computer Aided Verification
Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic
Andrew Reynolds et al. (2017) · 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Thomas Ströder et al. (2017) · Journal of Automated Reasoning
Completeness for recursive procedures in separation logic
Mahmudul Faisal Al Ameen et al. (2016) · Theoretical Computer Science
Completeness of Verification System with Separation Logic for Recursive Procedures
Mahmudul Faisal Al Ameen (2016)
Concurrent separation logic
Stephen Brookes et al. (2016) · ACM SIGLOG News
Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
Stéphane Demri et al. (2016) · ACM Transactions on Computational Logic
Completeness for a first-order abstract separation logic
Zhé Hóu et al. (2016) · 14th Asian Symposium on Programming Languages and Systems (APLAS)
Proof automation for functional correctness in separation logic
Ewen Maclean et al. (2016) · Journal of Logic and Computation
Viper: A verification infrastructure for permission-based reasoning
Peter Müller et al. (2016) · Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds et al. (2016) · Automated Technology for Verification and Analysis
Permission-based separation logic for multithreaded Java programs
Afshin Amighi et al. (2015) · Logical Methods in Computer Science
Witnessing the elimination of magic wands
Stefan Blom et al. (2015) · International Journal on Software Tools for Technology Transfer
Being and Change: Reasoning About Invariance
Frank S. de Boer et al. (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 et al. (2015) · 27th European Summer School in Logic, Language and Information (ESSLLI 2015)
Separation logics and modalities: a survey
Stéphane Demri et al. (2015) · Journal of Applied Non-Classical Logics
A Program Construction and Verification Tool for Separation Logic
Brijesh Dongol et al. (2015) · Mathematics of Program Construction
Foundations for Decision Problems in Separation Logic with General Inductive Predicates
Timos Antonopoulos et al. (2014) · Foundations of Software Science and Computation Structures
A Decision Procedure for Satisfiability in Separation Logic with Inductive Definitions
James Brotherston et al. (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)
A proof system for separation logic with magic wand
Wonyeol Lee et al. (2014) · ACM SIGPLAN Notices
Communicating state transition systems for fine-grained concurrent resources
Aleksandar Nanevski et al. (2014) · 23rd European Symposium on Programming Languages and Systems (ESOP)
Automating Separation Logic with Trees and Data
Ružica Piskač et al. (2014) · Computer Aided Verification
Completeness of separation logic with inductive definitions for program verification
Makoto Tatsuta et al. (2014) · International Conference on Software Engineering and Formal Methods
Satisfiability modulo abstraction for separation logic with linked lists
Aditya Thakur et al. (2014) · International SPIN Symposium on Model Checking of Software
A Simple Separation Logic
Andreas Herzig (2013) · Logic, Language, Information, and Computation
The Tree Width of Separation Logic with Recursive Definitions
Radu Iosif et al. (2013) · Automated Deduction – CADE-24
Automating Separation Logic Using SMT
Ružica Piskač et al. (2013) · Computer Aided Verification
Separation predicates: A taste of separation logic in first-order logic
François Bobot et al. (2012) · International Conference on Formal Engineering Methods
On the almighty wand
Rémi Brochenin et al. (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
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 et al. (2011) · The Journal of Logic and Algebraic Programming
Verification of programs in virtual memory using separation logic
Rafal Michal Kolanski (2011)
Undecidability of propositional separation logic and its neighbours
James Brotherston et al. (2010) · 25th IEEE Symposium on Logic in Computer Science (LICS)
Tableaux and resource graphs for separation logic
Didier Galmiche et al. (2010) · Journal of Logic and Computation
Design patterns in separation logic
Neelakantan R. Krishnaswami et al. (2009) · 4th International Workshop on Types in Language Design and Implementation
A Certified Verifier for a Fragment of Separation Logic
Nicolas Marti et al. (2009) · Information and Media Technologies
An Introduction to Separation Logic
John C. Reynolds (2009) · Engineering Methods and Tools for Software Safety and Security
Completeness of Pointer Program Verification by Separation Logic
Makoto Tatsuta et al. (2009) · 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods
Cyclic proofs of program termination in separation logic
James Brotherston et al. (2008) · ACM SIGPLAN Notices
jStar: Towards Practical Verification for Java
Dino Distefano et al. (2008) · Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications
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
Relational parametricity and separation logic
Lars Birkedal et al. (2007) · 10th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS)
A semantics for concurrent separation logic
Stephen Brookes (2007) · Theoretical Computer Science
Local reasoning about data update
Cristiano Calcagno et al. (2007) · Electronic Notes in Theoretical Computer Science
Local Action and Abstract Separation Logic
Cristiano Calcagno et al. (2007) · 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
Resources, concurrency, and local reasoning
Peter W. O'Hearn (2007) · Theoretical Computer Science
Types, bytes, and separation logic
Harvey Tuch et al. (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)
A Local Shape Analysis Based on Separation Logic
Dino Distefano et al. (2006) · Tools and Algorithms for the Construction and Analysis of Systems
Expressivity properties of Boolean BI through relational models
Didier Galmiche et al. (2006) · 26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
Verifying properties of well-founded linked lists
Shuvendu K. Lahiri et al. (2006) · ACM SIGPLAN Notices
Separation logic for higher-order store
Bernhard Reus et al. (2006) · 20th International Workshop on Computer Science Logic (CSL)
Symbolic Execution with Separation Logic
Josh Berdine et al. (2005) · Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings
Permission accounting in separation logic
Richard Bornat et al. (2005) · Proceedings of the 32nd ACM Symposium on Principles of Programming Languages
From separation logic to first-order logic
Cristiano Calcagno et al. (2005) · 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS)
A Decidable Fragment of Separation Logic
Josh Berdine et al. (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
Generalized Records and Spatial Conjunction in Role Logic
Viktor Kuncak et al. (2004) · Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings
On Spatial Conjunction as Second-Order Logic
Viktor Kuncak et al. (2004)
Extending Separation Logic with Fixpoints and Postponed Substitution
Élodie-Jane Sims (2004) · Algebraic Methodology and Software Technology
Towards mechanized program verification with separation logic
Tjark Weber (2004) · 18th International Workshop on Computer Science Logic (CSL)
A proof system for object oriented programming using separation logic
Ronald Middelkoop (2003)
The Semantics and Proof Theory of the Logic of Bunched Implications
David J. Pym (2002)
Separation logic: a logic for shared mutable data structures
John C. Reynolds (2002) · Proceedings 17th Annual IEEE Symposium on Logic in Computer Science
A Semantic Basis for Local Reasoning
Hongseok Yang et al. (2002) · Foundations of Software Science and Computation Structures
Computability and Complexity Results for a Spatial Assertion Language for Data Structures
Cristiano Calcagno et al. (2001) · Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
BI as an assertion language for mutable data structures
Samin S. Ishtiaq et al. (2001) · 28th ACM Symposium on Principles of Programming Languages (POPL)
Local Reasoning about Programs that Alter Data Structures
Peter W. O'Hearn et al. (2001) · Computer Science Logic
Local reasoning for stateful programs
Hongseok Yang (2001)
Proving pointer programs in Hoare logic
Richard Bornat (2000) · 5th International Conference on Mathematics of Program Construction (MPC)
Intuitionistic Reasoning about Shared Mutable Data Structure
John C. Reynolds (2000) · Millennial Perspectives in Computer Science
The logic of bunched implications
Peter W. O'Hearn et al. (1999) · Bulletin of Symbolic Logic
Static detection of pointer errors: an axiomatisation and a checking algorithm
Pascal Fradet et al. (1996) · European Symposium on Programming
Proving assertions about programs that manipulate data structures
Derek C. Oppen et al. (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