Relational thread-modular static value analysis by abstract interpretation

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 study thread-modular static analysis by abstract interpretation to infer the values of variables in concurrent programs. We show how to go beyond the state of the art and increase an analysis precision by adding the ability to infer some relational and history-sensitive properties of thread interferences. The fundamental basis of this work is the formalization by abstract interpretation of a rely-guarantee concrete semantics which is thread-modular, constructive, and complete for safety properties. We then show that previous analyses based on non-relational interferences can be retrieved as coarse computable abstractions of this semantics; additionally, we present novel abstraction examples exploiting our ability to reason more precisely about interferences, including domains to infer relational lock invariants and the monotonicity of counters. Our method and domains have been implemented in the AstréeA static analyzer that checks for run-time errors in embedded concurrent C programs, where they enabled a significant reduction of the number of false alarms.
Type de document :
Communication dans un congrès
Kenneth McMillan and Xavier Rival. VMCAI 2014 - 15th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2014, San Diego, United States. Springer, 8318, pp.39-58, 2014, 〈10.1007/978-3-642-54013-4_3〉
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-00925713
Contributeur : Antoine Miné <>
Soumis le : jeudi 30 janvier 2014 - 15:42:20
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : samedi 8 avril 2017 - 12:57:46

Fichier

article_ok.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Antoine Miné. Relational thread-modular static value analysis by abstract interpretation. Kenneth McMillan and Xavier Rival. VMCAI 2014 - 15th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2014, San Diego, United States. Springer, 8318, pp.39-58, 2014, 〈10.1007/978-3-642-54013-4_3〉. 〈hal-00925713〉

Partager

Métriques

Consultations de la notice

522

Téléchargements de fichiers

332