Le, QL;
(2021)
Compositional Satisfiability Solving in Separation Logic.
In: Henglein, F and Shoham, S and Vizel, Y, (eds.)
Verification, Model Checking, and Abstract Interpretation: 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings.
(pp. pp. 578-602).
Springer: Cham, Switzerland.
Preview |
Text
s2s-vmcai2021.pdf - Accepted Version Download (387kB) | Preview |
Abstract
We introduce a novel decision procedure to the satisfiability problem in array separation logic combined with general inductively defined predicates and arithmetic. Our proposal differentiates itself from existing works by solving satisfiability through compositional reasoning. First, following Fermat’s method of infinite descent, it infers for every inductive definition a “base” that precisely characterises the satisfiability. It then utilises the base to derive such a base for any formula where these inductive predicates reside in. Especially, we identify an expressive decidable fragment for the compositionality. We have implemented the proposal in a tool and evaluated it over challenging problems. The experimental results show that the compositional satisfiability solving is efficient and our tool is effective and efficient when compared with existing solvers.
| Type: | Proceedings paper |
|---|---|
| Title: | Compositional Satisfiability Solving in Separation Logic |
| Event: | VMCAI 2021: Verification, Model Checking, and Abstract Interpretation |
| ISBN-13: | 9783030670665 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-67067-2_26 |
| Publisher version: | https://doi.org/10.1007/978-3-030-67067-2_26 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10146153 |
Archive Staff Only
 |
View Item |
