Relational thread-modular static value analysis by abstract interpretation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Relational thread-modular static value analysis by abstract interpretation

Résumé

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.
Fichier principal
Vignette du fichier
article_ok.pdf (372.05 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00925713 , version 1 (30-01-2014)

Identifiants

Citer

Antoine Miné. Relational thread-modular static value analysis by abstract interpretation. VMCAI 2014 - 15th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2014, San Diego, United States. pp.39-58, ⟨10.1007/978-3-642-54013-4_3⟩. ⟨hal-00925713⟩
339 Consultations
517 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More