CEA List

FLUCTUAT is a static analysis tool, using abstract interpretation, of C and ADA source code. It automatically determines over approximations of values that program variables can take, for all possible executions, as well as over-approximations of the computation inaccuracies.

By computation inaccuracy, we mean the difference between the computation in real numbers, with the one in floating-point numbers (IEEE 754 , MIL1750...standards). Moreover, this computation inaccuracy is decomposed over the lines of the program under analysis in order to give some indication to the end-user about the possible causes of the loss of the precision.

FLUCTUAT also proves functional properties of a program, both on the underlying algorithmics it implements (using the real number semantics, allowing for characterizing the model error) and on the implementation (using the floating-point semantics). It can provide for worst-case test generation (maximum error, maximum value etc.). It also propagates model and input (coming from sensor for instance) uncertainties and provides for sensitivity analyzes. It contains also an extension for doing these analyzes on hybrid models, based on a program and a model of a physical environment, given by a set (possibly switched) differential equations.

FLUCTUAT is based on an abstract domain which expresses relational properties between values of variables. The analysis is parameterizable and its results can be visualized using a GUI. An assertion language can be used to specify the inputs of the program under analysis.

• Visit: www-list.cea.fr