Two-Variable Separation Logic and Its Inner Circle
Abstract
Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the smallest fragments of separation logic known to be undecidable, and this contrasts with the decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with nonelementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional interval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely related logics.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Mar 21, 2015
- Source ID
- 10.1145/2724711
Entities
People
- Morgan Deters
- Stéphane Demri
Organizations
- Air Force Office of Scientific Research
- National Science Foundation
- New York University
- Seventh Framework Programme