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

Antoine Miné 1, 2
1 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
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.
Type de document :
Communication dans un congrès
Pierre-Alain Reynier. 10th School of Modelling and Verifying Parallel Processes, Dec 2012, Marseille, France. 2012
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00763076
Contributeur : Antoine Miné <>
Soumis le : lundi 10 décembre 2012 - 10:08:22
Dernière modification le : mardi 24 avril 2018 - 17:20:15
Document(s) archivé(s) le : samedi 17 décembre 2016 - 23:10:59

Fichier

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

Identifiants

  • HAL Id : hal-00763076, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

388

Téléchargements de fichiers

199