Paper Info
Title
Proving Guarantee And Recurrence Temporal Properties By Abstract Interpretation
Abstract
We present new static analysis methods for proving liveness properties of programs. In particular, with reference to the hierarchy of temporal properties proposed by Manna and Pnueli, we focus on guarantee (i.e., "something good occurs at least once") and recurrence (i.e., "something good occurs infinitely often") temporal properties.We generalize the abstract interpretation framework for termination presented by Cousot and Cousot. Specifically, static analyses of guarantee and recurrence temporal properties are systematically derived by abstraction of the program operational trace semantics.These methods automatically infer sufficient preconditions for the temporal properties by reusing existing numerical abstract domains based on piecewise-defined ranking functions. We augment these abstract domains with new abstract operators, including a dual widening.To illustrate the potential of the proposed methods, we have implemented a research prototype static analyzer, for programs written in a C-like syntax, that yielded interesting preliminary results.
Year
DOI
Venue
2015
10.1007/978-3-662-46081-8_11
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2015)
Field
DocType
Volume
Abstraction,Ranking,Abstract interpretation,Computer science,Static analysis,Theoretical computer science,Operator (computer programming),Hierarchy,Semantics,Liveness
Conference
8931
ISSN
Citations 
PageRank 
0302-9743
5
0.42
References 
Authors
19
2
Name
Order
Citations
PageRank
Caterina Urban1795.39
Antoine Miné2111751.15