Skip to Main content Skip to Navigation
Conference papers

Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs

Antoine Miné 1, 2 
2 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
Abstract : We present a static analysis by Abstract Interpretation to check for run-time errors in parallel C programs. Following our work on Astrée, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads. Our method iterates a slightly modified non-parallel analysis over each thread in turn, until thread interferences stabilize. We prove the soundness of the method with respect to a sequential consistent semantics and a reasonable weakly consistent memory semantics. We then show how to take into account mutual exclusion and thread priorities through partitioning over the scheduler state. We present preliminary experimental results analyzing a real program with our prototype, Thésée, and demonstrate the scalability of our approach.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Sunday, December 4, 2011 - 11:18:13 PM
Last modification on : Thursday, March 17, 2022 - 10:08:36 AM
Long-term archiving on: : Friday, November 16, 2012 - 2:21:24 PM


Files produced by the author(s)




Antoine Miné. Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs. ESOP'11 - 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. pp.398-418, ⟨10.1007/978-3-642-19718-5_21⟩. ⟨hal-00648038⟩



Record views


Files downloads