Paper Info
Title
Abstract Interpretation of CTL Properties.
Abstract
CTL is a temporal logic commonly used to express program properties. Most of the existing approaches for proving CTL properties only support certain classes of programs, limit their scope to a subset of CTL, or do not directly support certain existential CTL formulas. This paper presents an abstract interpretation framework for proving CTL properties that does not suffer from these limitations. Our approach automatically infers sufficient preconditions, and thus provides useful information even when a program satisfies a property only for some inputs. We systematically derive a program semantics that precisely captures CTL properties by abstraction of the operational trace semantics of a program. We then leverage existing abstract domains based on piecewise-defined functions to derive decidable abstractions that are suitable for static program analysis. To handle existential CTL properties, we augment these abstract domains with under-approximating operators. We implemented our approach in a prototype static analyzer. Our experimental evaluation demonstrates that the analysis is effective, even for CTL formulas with non-trivial nesting of universal and existential path quantifiers, and performs well on a wide variety of benchmarks.
Year
DOI
Venue
2018
10.1007/978-3-319-99725-4_24
Lecture Notes in Computer Science
Field
DocType
Volume
Static program analysis,Abstraction,Abstract interpretation,Computer science,Decidability,Theoretical computer science,Operator (computer programming),Temporal logic,CTL*,Semantics
Conference
11002
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
22
3
Name
Order
Citations
PageRank
Caterina Urban1795.39
Samuel Ueltschi200.34
Peter Müller378150.82