Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation

Caterina Urban 1 Antoine Miné 1
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
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.
Type de document :
Communication dans un congrès
16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'15), Jan 2015, Mumbai, India. Springer, 8931, pp.19, Lecture Notes in Computer Science. 〈http://research.microsoft.com/〉. 〈10.1007/978-3-662-46081-8_11〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01105238
Contributeur : Antoine Miné <>
Soumis le : mardi 20 janvier 2015 - 15:40:19
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : mardi 21 avril 2015 - 10:15:28

Fichier

article-urban-mine-vmcai15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Caterina Urban, Antoine Miné. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'15), Jan 2015, Mumbai, India. Springer, 8931, pp.19, Lecture Notes in Computer Science. 〈http://research.microsoft.com/〉. 〈10.1007/978-3-662-46081-8_11〉. 〈hal-01105238〉

Partager

Métriques

Consultations de la notice

272

Téléchargements de fichiers

113