Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée

Antoine Miné (1) , Laurent Mauborgne (2) , Xavier Rival (3, 4) , Jerome Feret (3, 4) , Patrick Cousot (5, 4) , Daniel Kästner (2) , Stephan Wilhelm (2) , Christian Ferdinand (2)

1 APR - Algorithmes, Programmes et Résolution
2 Angewandte Informatik - AbsInt GmbH
3 LIENS - Laboratoire d'informatique de l'école normale supérieure
4 ANTIQUE - Analyse Statique par Interprétation Abstraite
5 CIMS - Courant Institute of Mathematical Sciences [New York]

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.

Domaines: Systèmes embarqués

Antoine Miné, Laurent Mauborgne, Xavier Rival, Jerome Feret, Patrick Cousot, et al.. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Jan 2016, Toulouse, France. ⟨hal-01271552⟩