Abstract:
We describe the structure of abstract domains in Astrée,
their modular organization into a hierarchical network, their cooperation
to over-approximate the conjunction/reduced product of different
abstractions, and to ensure termination using collaborative widenings
and narrowings. This separation of the abstraction into a combination
of cooperative abstract domains makes Astrée extensible, an essential
feature to cope with false alarms and ultimately provide sound formal
verifications of the absence of runtime errors in very large software.
\bibitem{ccfmmmr08}
{\sc Cousot, P., Cousot, R., Feret, J., Min{\'e}, A., Mauborgne, L., Monniaux,
D., and Rival, X.}
\newblock Combination of abstractions in the astrÉe static analyzer.
\newblock In {\em Advances in Computer Science - ASIAN 2006. Secure Software
and Related Issues\/} (2008), vol.~4435 of {\em Lecture Notes in Computer
Science}, Springer-Verlag, pp.~272--300.
@inproceedings{ccfmmmr08,
author = "Patrick Cousot and Radhia Cousot and J{\'e}r{\^o}me Feret and
Antoine Min{\'e} and Laurent Mauborgne and David Monniaux and
Xavier Rival",
title = "Combination of Abstractions in the ASTRÉE Static Analyzer",
booktitle = "Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = 4435,
pages = "272-300",
year = 2008,
}