Skip to Main content Skip to Navigation
Conference papers

Static Analysis by Abstract Interpretation of Sequential and Multi-Thread Programs

Antoine Miné 1, 2 
1 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
2 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
Abstract : In the realm of embedded critical systems, it is crucial to guarantee the correctness of programs before they are deployed. Static analyzers can help by detecting at compile-time potentially erroneous program behaviors: they perform sound over-approximations to achieve an efficient analysis while not missing any potential behavior. We discuss the systematic design of such analyzers using abstract interpretation, a general theory of semantic approximation. After recalling the classic construction of static analyzers for sequential programs by abstraction of the concrete trace semantics, we introduce abstractions to derive thread-modular analyzers for multithreaded programs, borrowing ideas from rely/guarantee proof methods. Finally, we present two static analyzer tools, Astrée and AstréeA, that are used to check for run-time errors in large sequential and multithreaded embedded industrial avionic C applications.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Monday, December 10, 2012 - 10:08:22 AM
Last modification on : Thursday, March 17, 2022 - 10:08:48 AM
Long-term archiving on: : Saturday, December 17, 2016 - 11:10:59 PM


Files produced by the author(s)


  • HAL Id : hal-00763076, version 1



Antoine Miné. Static Analysis by Abstract Interpretation of Sequential and Multi-Thread Programs. 10th School of Modelling and Verifying Parallel Processes, Dec 2012, Marseille, France. ⟨hal-00763076⟩



Record views


Files downloads