A decision procedure for satisfiability in separation logic with inductive predicates
- Submitting institution
-
Birkbeck College
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 12345
- 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
- 25:1
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- July
- Year of publication
- 2014
- URL
-
https://dl.acm.org/doi/10.1145/2603088.2603091
- 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)
-
1 - Algorithms, Verification and Software
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Open-source implementation of the decision procedure is available at <https://github.com/ngorogiannis/cyclist/releases/>. Its implementation in the open-source program analysis tool Cyclist scored highest in division qf_shid_sat at the Separation Logic Competition (SL-COMP) in 2018: <https://www.irif.fr/~sighirea/sl-comp/18/qf_shid_sat.html>. The paper provides the basis for further publications on abduction of predicates (SAS'14, <https://doi.org/10.1007/978-3-319-10936-7_5>), disproving inductive entailments (TABLEAUX'15, <https://doi.org/10.1007/978-3-319-24312-2_20>), model checking (POPL'16, <https://doi.org/10.1145/2837614.2837621>), and decision procedures for an extension with a fragment of Presburger arithmetic (APLAS'17, <https://doi.org/10.1007/978-3-319-47958-3_22>).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -