Inference of ranking functions for proving temporal properties by abstract interpretation

Caterina Urban 1, 2 Antoine Miné 2, 3
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
3 APR - Algorithmes, Programmes et Résolution
LIP6 - Laboratoire d'Informatique de Paris 6
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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [35 references]  Display  Hide  Download

https://hal.sorbonne-universite.fr/hal-01312239
Contributor : Antoine Miné <>
Submitted on : Thursday, May 5, 2016 - 9:09:34 AM
Last modification on : Friday, March 22, 2019 - 1:42:20 AM
Long-term archiving on: Tuesday, November 15, 2016 - 8:37:40 PM

File

article-urban-mine-comlan2015....
Files produced by the author(s)

Identifiers

Citation

Caterina Urban, Antoine Miné. Inference of ranking functions for proving temporal properties by abstract interpretation. Computer Languages, Systems and Structures, Elsevier, 2015, ⟨10.1016/j.cl.2015.10.001⟩. ⟨hal-01312239⟩

Share

Metrics

Record views

568

Files downloads

275