Skip to Main content Skip to Navigation
Conference papers

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 - ENS Paris, 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.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Thursday, January 30, 2014 - 3:42:20 PM
Last modification on : Thursday, March 17, 2022 - 10:08:43 AM
Long-term archiving on: : Saturday, April 8, 2017 - 12:57:46 PM


Files produced by the author(s)




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⟩



Record views


Files downloads