about this paper

presentation abstract bibitem

downloads

paper (on HAL)
Antoine Miné, Laurent Mauborgne, Xavier Rival, Jérôme Feret, Patrick Cousot, Daniel Kästner, Stephan Wilhelm, and Christian Ferdinand.
Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée.
In Embedded Real Time Software and Systems - ERTSS 2016.

Abstract: We present an extension of Astrée to concurrent C software. Astr�e is a sound static analyzer for run-time errors previously limited to sequential C software. Our extension employs a scalable abstraction which covers all possible thread interleavings, and soundly reports all run-time errors and data races: when the analyzer does not report any alarm, the program is proven free from those classes of errors. We show how this extension is able to support a variety of operating systems (such as POSIX threads, ARINC 653, OSEK/AUTOSAR) and report on experimental results obtained on concurrent software from different domains, including large industrial software. 

@inproceedings{erts10,
    author    = "Antoine Min{\'e}, Laurent Mauborgne, Xavier Rival,
J{\'e}r{\^o}me Feret, Patrick Cousot, Daniel K{\"a}stner, Stephan Wilhelm, and Christian Ferdinand",
    title     = "Analysis to the Next Level: Proving the Absence of Run-Time Errors and
Data Races with Astr{\'e}e",
    booktitle = "Embedded Real Time Software and Systems - ERTSS 2016",
    year = 2016,
}