about this paper

presentation abstract bibitem

downloads

paper (on HAL)
Daniel Kästner, Christian Ferdinand, Stephan Wilhelm, Stefana Nenova, Olha Honcharova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival, and Élodie-Jane Sims.
Astrée: Nachweis der Abwesenheit von Laufzeitfehlern.
In Workshop "Entwicklung zuverl�ssiger Software-Systeme", Regensburg, Germany, June 18th, 2009.

Abstract: Sicherheitskritische eingebettete Systeme m�ssen hohen Qualit�tsanforderungen gen�gen. Laufzeitfehler, z.B. arithmetische �berl�ufe oder Rundungsfehler k�nnen zu fehlerhaftem Programmverhalten f�hren. Da in der Regel keine vollst�ndige Testabdeckung m�glich ist, bieten sich statische Analysatoren an. Diese bieten eine vollst�ndige Coverage, k�nnen jedoch Fehlalarme erzeugen. Da jeder potentielle Laufzeitfehler manuell vom Benutzer �berpr�ft werden muss, kann eine hohe Zahl von Fehlalarmen dazu f�hren, dass echte Fehler �bersehen werden. Der statische Analysator Astr�e kann durch Spezialisierung und Parametrisierung an die zu analysierende Software angepasst werden. Dies erm�glicht kurze Analysezeiten und eine niedrige Zahl von Fehlalarmen. Astr�e wird z.B. bei der Zertifizierung von industrieller Flugzeugsteuerungssoftware eingesetzt. Safety-critical embedded software has to satisfy stringent quality. 

@InProceedings{KastnerEtAl-09,
   author =    {D.~K\"astner and C.~Ferdinand and S.~Wilhelm and S.~Nevona and O.~Honcharova and
                P.~Cousot and R.~Cousot and J.~Feret and L.~Mauborgne and A.~Min\'e and
                X.~Rival and \'E.-J.~Sims},
   title =     {\textsc{Astr\'ee}: Nachweis der Abwesenheit von Laufzeitfehlern},
   booktitle = {Workshop ``Entwicklung zuverl\"assiger Software-Systeme''},
   address =   {Regensburg, Germany},
   month =     {18 June},
   year =      2009,
}