FLUCTUAT

FLUCTUAT is an abstract-interpretation based static analyzer of numerical programs (C or Ada) developed since 2001 by the MEASI (ModElling and Analysis of Systems in Interaction) laboratory of CEA-LIST. Given sets of inputs and parameters, possibly entached by uncertainties, it considers all possible behaviours of the program both in real and in finite precision, and characterizes the differences.

Have a look at our small leaflet and our APLAS 2013 poster.

Foundations of FLUCTUAT

Objectives

FLUCTUAT takes as input a program (in C or Ada), possibly annotated with assertions specifying for instance bounds on input values or parameters, and uncertainties on these values. It outputs guaranteed bounds for all variable values, considered both with a real and a finite precision (floating-point) semantics, for all possible executions given the sets of inputs and parameters. It also bounds the error due to rounding errors in computations or uncertainties on inputs, and decomposes this error along its provenance in the source code: it presents this information graphically (on a graph which abscissa is the line number in the source code and ordinate is the amplitude of the error), in order to point out the main sources of errors.
Further usages include verifying functional properties of the algorithm (the method error), by setting assertions characterizing properties that should be satisfied by a part of a program; or generating worst test case, that will confirm that some bounds given by the analysis can indeed be reached (or nearly so).

The abstract domains

FLUCTUAT relies on zonotopic abstract domains, which we have studied quite in depth these last ten years. They can be used as non specialized abstract domains for numerical program analysis, as described for instance in our SAS'06, CAV'09, and CAV'10 papers.
They can also be extended to abstract finite precision computations, as implemented in FLUCTUAT and partially described in this VMCAI'11 paper. And we finally use them for robustness and unstable tests analysis (see APLAS'13 paper and extended version).

Current extensions

We extended these domains to compute inner (or under) approximation of values of program variables, first version in a SAS'07 paper, and more recently in a HSCC'14 paper. Inner approximations (sets of values that we are sure to be reached for some inputs in the given range) can for instance guarantee that something bad will happen, or simply give indication on the quality of the approximation by the distance between inner and outer (or over) approximations. This extension is not yet implemented in Fluctuat, but we are thinking of it.
We are also interested in mixing probabilistic and non-deterministic information: we defined for that a first abstraction by probabilistic affine forms (see here and there), which was for now experimented on a separate prototype.
Our zonotopic abstract domain define abstraction of input-output relations: they are thus naturally well suited for modular analysis, as was reported in a SAS'12 paper.

External libraries

FLUCTUAT is written in C++. Its numerical computations rely on the GNU MPFR Library for multiple-precision floating-point computations with correct rounding. We also use the Incredible XML Parser. The user interface uses Qt designer.

You can find here more publications and projects around Fluctuat.

Using FLUCTUAT

Some industrial case studies

The primary applications of FLUCTUAT are the analysis of safety-critical embedded, and more generally control software. Here are some publications (FMICS'07, FMICS'09 and DASIA'09) illustrating case studies that have been conducted in the context of nuclear, avionic and space applications.
We are also naturally interested by the analysis of programs from scientific computing: we had first positive experiments on the solution of linear systems by conjugate gradient algorithms, and would like to extend the class of problems handled.

Videos demonstrating the use of FLUCTUAT

• A motivating example: non linear iterative program that computes a square root, with cubic convergence in real numbers, but which does not always terminate in floating point numbers, because the stopping criterion is not well suited to simple precision
• Use of Fluctuat on the above example: on a restricted range here, but this comes from a real case study - see FMICS'07 paper
• Set of parametrized filters: static analysis (fixed point computation), worst case generation, see FMICS'09 paper
• Functional verification of elementary functions: linked to the FMICS'09 paper)
• Extension to hybrid systems: linked to the CAV'09 and DASIA'09 papers: first extension of Fluctuat towards hybrid systems, and application to a case study from aerospace
• If you want want more...

Contact

We look forward to research collaborations around these themes. An academic version of Fluctuat is available upon request. A first natural use is either through the Fluctuat graphical interface, or in batch mode. But we also have an API, and an interactive version available.
We also welcome internship and PhD candidates.

Please contact us: franck.vedrine at cea.fr or eric.goubault at polytechnique.edu or sylvie.putot at polytechnique.edu.