Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival, Static Analysis and Verification of Aerospace Software by Abstract Interpretation

Antoine Miné, Laurent Mauborgne, Xavier Rival, Jérôme Feret, Patrick Cousot, Daniel Kästner, Stephan Wilhelm, Christian Ferdinand.
Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée
In 8^th European Congress on Embedded Real–Time Software and Systems, Toulouse, 27—29 January 2016, France, http://www.erts2016.org/programme-thursday.html#th.4.c.
Paper:
- PDF (539 KB)
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.
Keywords:
Abstract interpretation, ARINC 653, Astrée, C, Concurrency, OSEK/AUTOSAR, Parallelism, POSIX threads, Static Analysis,

Bibliographic reference:

@inproceedings{MineEtAl-ERTCS-2016,
  author    = {Antoine Min{\'e}, Laurent Mauborgne, Xavier Rival, J{\'e}r{\^o}me Feret, Patrick Cousot, 
               Daniel K{\"a}stner, Stephan Wilhelm, Christian Ferdinand},
  title     = {Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astr{\'e}e},
  journal   = {8$^{\mathrm{th}}$ European Congress on Embedded Real-Time Software and Systems, Toulouse, France},
  month     = jan,
  year      = {2016},
  url       = {http://www.erts2016.org/programme-thursday.html#th.4.c}
 }

\bibitem{{MineEtAl-ERTCS-2016}
Antoine Miné, Laurent Mauborgne, Xavier Rival, Jérôme Feret, Patrick Cousot, 
Daniel Kästner, Stephan Wilhelm, Christian Ferdinand.
\newblock Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and 
          Data Races with Astrée.
\newblock In \emph{8$^{\mathrm{th}}$ European Congress on Embedded Real-Time Software and Systems},
          Toulouse, 27--29 January 2016, France,
          \url{http://www.erts2016.org/programme-thursday.html#th.4.c}.

copyright notice,
Last modified: Sun Oct 16 10:44:07 EDT 2016