2015 | OriginalPaper | Chapter
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation
Authors : Caterina Urban, Antoine Miné
Published in: Verification, Model Checking, and Abstract Interpretation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.