Paper Info
Title
On Automation Of Ctl* Verification For Infinite-State Systems
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 CTL* 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.
Year
DOI
Venue
2015
10.1007/978-3-319-21690-4_2
COMPUTER AIDED VERIFICATION, PT I
Field
DocType
Volume
Computation tree logic,Quantifier elimination,Program transformation,Programming language,Model checking,Computer science,Algorithm,Precondition,Theoretical computer science,Mathematical proof,Operator (computer programming),CTL*
Conference
9206
ISSN
Citations 
PageRank 
0302-9743
13
0.53
References 
Authors
15
3
Name
Order
Citations
PageRank
Byron Cook1605.08
heidy khlaaf2161.25
Nir Piterman3115470.02