zbMATH — the first resource for mathematics

Automatically verifying temporal properties of pointer programs with cyclic proof. (English) Zbl 06778422
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-63045-8/pbk; 978-3-319-63046-5/ebook). Lecture Notes in Computer Science 10395. Lecture Notes in Artificial Intelligence, 491-508 (2017).
Summary: 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 modalities 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 nondeterministic 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.
For the entire collection see [Zbl 1369.68037].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI