Tellez, G; Brotherston, J; (2019) Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. Journal of Automated Reasoning 10.1007/s10817-019-09532-0. (In press).

Preview

Text Automatically Verifying Temporal Properties of Pointer.pdf - Published Version Download (1MB) | Preview

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.

Download activity - last month

Export as XMLJSONCSV

Download activity - last 12 months

Export as CSVJSONXML

Downloads by country - last 12 months

Export as CSVJSONXML

Archive Staff Only

View Item