@inproceedings{bou-con-cou-cou-fer-gho-09-aa-space,
  author = {Bouissou, Olivier and Conquet, {\'E}ric and Cousot, Patrick and Cousot, Radhia and Feret, J{\'e}r{\^o}me and Ghorbal, Khalil and Goubault, {\'E}ric and Lesens, David and Mauborgne, Laurent and Min{\'e}, Antoine and Putot, Sylvie and Rival, Xavier and Turin, Michel},
  title = {Space Software Validation using Abstract Interpretation},
  booktitle = {Proceedings of the International Space System Engineering Conference - Data Systems in Aerospace (DASIA)},
  location = {Istambul, TR},
  month = may,
  pages = {1-7},
  year = 2009,
  url = {https://hal.inria.fr/inria-00528590/},
  comment = {Describes two tools, including FLUCTUAT, that uses AA. FLUCTUAT `` produces a graphical representation of the source of each numerical precision loss. It allows the user to know quickly the lines in the C source code causing the biggest losses of numerical precision. For loops, the tool also allows to produce graphics representing the evolution of bounds for the values and errors of variables during the computation.''},
  abstract = {This paper reports the results of an ESA funded project on the use of abstract interpretation to validate critical real-time embedded space software. Abstract interpretation is industrially used since several years, especially for the validation of the Ariane 5 launcher. However, the limitations of the tools used so far prevented a wider deployment. Astrium Space Transportation, CEA, and ENS have analyzed the performances of two recent tools on a case study extracted from the safety software of the ATV: * ASTR{\'E}E, developed by ENS and CNRS, to check for run-time errors, * FLUCTUAT, developed by CEA, to analyse the accuracy of numerical computations. The conclusion of the study is that the performance of this new generation of tools has dramatically increased (no false alarms and fine analysis of numerical precision).}
  quotes = {This paper reports the results of an ESA funded project on the use of abstract interpretation to validate critical real-time embedded space software. Abstract interpretation is industrially ...}
}