Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
Abstract
Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, we show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak second-order logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these and, as a by-product, identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction. Because we forbid ourselves the use of many syntactic resources, this underscores even further the power of separating implication on concrete heaps.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 07, 2016
- Source ID
- 10.1145/2835490
Entities
People
- Morgan Deters
- Stéphane Demri
Organizations
- Air Force Office of Scientific Research
- National Science Foundation
- New York University
- Paris-Saclay University
- Seventh Framework Programme