Static analyzers like Astrée are incomplete, hence, may produce false alarms. We propose a framework for the investigation of the alarms produced by Astrée, so as to help classifying them as true errors or false alarms that are due to the approximation inherent in the static analysis. Our approach is based on the computation of an approximation of a set of traces specified by an initial and a (set of) final state(s). Moreover, we allow for finer analyses to focus on some execution patterns or on some possible inputs. The underlying algorithms were implemented inside Astrée and used successfully to track alarms in large, critical embedded applications. postscript , compressed postscript , PDF , compressed PDF

@InProceedings{xr:05:sas,
  author =       {X{.} Rival},
  title =        {Understanding the origin of alarms in {\sc Astr\'ee}},
  booktitle =    {12th Static Analysis Symposium (SAS'05)},
  pages =        {303--319},
  year =         {2005},
  volume =       {3672},
  series =       {LNCS},
  address =      {London (UK)},
  month =        sep,
  publisher =    {Springer}
}