Please use this identifier to cite or link to this item:
Title: On Automation of CTL* Verification for Infinite-State Systems
Authors: Cook, B.
Khlaaf, H.
Piterman, Nir
First Published: 16-Jul-2015
Presented at: Computer Aided Verification, San Francisco, CA, USA
Start Date: 18-Jul-2015
End Date: 24-Jul-2015
Publisher: Springer-Verlag
Citation: Springer Verlag (Germany)
Abstract: In this paper we introduce the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs. The method uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within \ctlstar proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We show the viability of our approach in practice using examples drawn from device drivers and various industrial examples.
DOI Link: 10.1007/978-3-319-21690-4_2
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Archived with reference to SHERPA/RoMEO and publisher website. The final publication is available at Springer via
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
paper.pdfPost-review (final submitted)442.94 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.