Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

09.08.2019 | Ausgabe 3/2020 Open Access

Journal of Automated Reasoning 3/2020

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 3/2020
Autoren:
Gadi Tellez, James Brotherston
Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

In this article, we investigate the automated verification of temporal properties of heap-aware programs. We propose a deductive reasoning approach based on cyclic proof. Judgements in our proof system assert that a program has a certain temporal property over memory state assertions, written in separation logic with user-defined inductive predicates, while the proof rules of the system unfold temporal modalities and predicate definitions 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 versions of the system 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 pointer programs. Experimental evaluation of our tool indicates that our approach is viable, and offers an interesting alternative to traditional model checking techniques.
Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner