@inproceedings{gou-13-aa-fluctuat,
  author = {Goubault, Eric},
  title = {Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and {FLUCTUAT}},
  booktitle = {Proc. International Static Analysis Symposium (SAS 2013)},
  year = 2013,
  publisher = {Springer},
  pages = {1--3},
  isbn = {978-3-642-38856-9},
  doi = {10.1007/978-3-642-38856-9_1},
  comment = {Invited lecture, survey of Goubault's work.  Calls affine forms `zonotopes'. The {FLUCTUAT} tool.},
  abstract = {This invited lecture is a survey of our work over the last 12 years or so, dealing with the precise analysis of numerical programs, essentially control programs such as the ones found in the aerospace, nuclear and automotive industry. Our approach is now based on a rather generic abstract domain, based on “zonotopes” or “affine forms” [7], but with some specificities. For instance, our zonotopic domain provides a functional abstraction [16,13], i.e. an abstraction of the input-output relationships between values of variables, allowing for test generation and modular verification [21]. Also, our domain deals with the real number and the finite precision (for instance, floating-point or fixed-point) semantics [14,17]. It is used in practice in FLUCTUAT [20,9,4] to prove some functional properties of programs, generate (counter-) examples, identify the discrepancy between the real number and the finite precision semantics and its origin etc.}
}