A decision procedure for satisfiability in separation logic with inductive predicates
- Submitting institution
-
Middlesex University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1329
- Type
- E - Conference contribution
- DOI
-
10.1145/2603088.2603091
- Title of conference / published proceedings
- 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) - CSL-LICS '14
- First page
- 1
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- July
- Year of publication
- 2014
- URL
-
http://eprints.mdx.ac.uk/15928/
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Adding user-defined inductive predicates to separation logic, a popular formalism for verifying pointer programs, allows one to express a wide class of memory data structures. This paper shows for the first time that satisfiability in the resulting logic is decidable, with a precise complexity bound (EXPTIME), and provides an implementation of the decision problem. The paper is significant because it shows the symbolic heap fragment of separation logic with general inductive predicates is satisfiable. The decision method has since been built on by several other authors and was still highly competitive in the most recent Separation Logic Competition (SL-COMP'19).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -