Tellez Espinosa, Gadi de Leon; (2019) Automatically Verifying Temporal Properties of Heap Programs with Cyclic Proof. Doctoral thesis (Ph.D), UCL (University College London).

Preview

Text Main.pdf - Accepted Version Download (1MB) | Preview

Abstract

This work proposes 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, given a suitable precondition, and whose rules operate directly on the temporal modalities as well as symbolically executing programs. Cyclic proofs in our system are, as elsewhere, finite rooted proof graphs subject to a natural, decidable sound ness condition, encoding a form of proof by infinite descent. We present two variants of our proof system, one for CTL (branching time) properties and one for LTL (linear time) properties, and show them both to be sound. We have implemented both variants in the C YCLIST theorem prover, yielding an automated tool that is capable of automatically discovering proofs of temporal properties of our programs. Evaluation of our tool on well-known benchmarks in the model checking community indicates that our approach is viable, and offers an interesting alternative to traditional model checking techniques.

Download activity - last month

Export as JSONXMLCSV

Download activity - last 12 months

Export as CSVXMLJSON

Downloads by country - last 12 months

Export as CSVXMLJSON

Archive Staff Only

View Item