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.
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).
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
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).
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.
You can find here more publications and projects around Fluctuat.
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.
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: eric.goubault at cea.fr or sylvie.putot at cea.fr.