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 de l'École normale supérieure, 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

https://hal.inria.fr/hal-00763076
Contributor : Antoine Miné <>
Submitted on : Monday, December 10, 2012 - 10:08:22 AM
Last modification on : Thursday, July 1, 2021 - 5:58:03 PM
Long-term archiving on: : Saturday, December 17, 2016 - 11:10:59 PM

File

paper_ok.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00763076, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

497

Files downloads

401