Tellez, G;
Brotherston, J;
(2017)
Automatically verifying temporal properties of pointer programs with cyclic proof.
In: De Moura, L, (ed.)
Automated Deduction – CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings.
(pp. pp. 491-508).
Springer: Cham, Switzerland.
Preview |
Text
cade.pdf - Accepted Version Download (579kB) | Preview |
Abstract
We propose a deductive reasoning approach to the automatic verification of temporal properties of pointer programs, based on cyclic proof. We present a proof system whose judgements express that a program has a certain temporal property over memory state assertions in separation logic, and whose rules operate directly on the temporal modal-ities as well as symbolically executing programs. Cyclic proofs in our system are, as usual, finite proof graphs subject to a natural, decidable soundness condition, encoding a form of proof by infinite descent. We present a proof system tailored to proving CTL properties of non-deterministic pointer programs, and then adapt this system to handle fair execution conditions. We show both systems to be sound, and provide an implementation of each in the Cyclist theorem prover, yielding an automated tool that is capable of automatically discovering proofs of (fair) temporal properties of heap-aware programs. Experimental evaluation of our tool indicates that our approach is viable, and offers an interesting alternative to traditional model checking techniques.
| Type: | Proceedings paper |
|---|---|
| Title: | Automatically verifying temporal properties of pointer programs with cyclic proof |
| Event: | 26th International Conference on Automated Deduction (CADE 26) |
| ISBN-13: | 9783319630458 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-63046-5_30 |
| Publisher version: | https://doi.org/10.1007/978-3-319-63046-5_30 |
| 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 UCL > Provost and Vice Provost Offices > UCL BEAMS 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 |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/1559240 |
Archive Staff Only
 |
View Item |
