about this paper

presentation abstract bibitem

downloads

paper editor link
Antoine Min�, Laurent Mauborgne, Xavier Rival, J�r�me Feret, Patrick Cousot, Daniel K�stner, Stephan Wilhelm, and Christian Ferdinand.
Stefana Nenova, Patrick Cousot, Radhia Cousot, J�r�me Feret, Laurent Mauborgne, Antoine Min� and Xavier Rival.
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",
    booktitle = "Embedded Real Time Software and Systems - ERTSS 2016",
    year = 2016,
}