Driving Frama-C's Value Analysis Towards a User Specified Goal

SPALTER is a Frama-C plug-in that iteratively improves the precision of Frama-C's value analysis results. It uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic and instructs Frama-C to execute case analyses that reintroduce previously ignored relations.

Although SPALTER currently only exists as a prototype, it automatically reproduces two Frama-C case studies (I, II), one of which required significant user interaction.

SPALTER was initially created during an internship of Sven Mattsen with the CEA List, supervised by Pascal Cuoq.

 
The video below shows SPALTER applied to the donut example. The Y axis of the graph represents possible values for the maximum of the function. 
Each dot represents an (input dimension-4 cube, output interval) pair from the worklist. The algorithm consumes limiting pairs (that is, dots from the topmost line). The resulting sub-divided dimension-4 cubes hopefully allow to compute a lower maximum, making other lines grow. 
On the right-hand side, the current best estimate for the maximum is the value of "Currgoal". When an entire line has been consumed, this value improves. "Currborder" is the best known minimum value for the maximum. The input dimension-4 cubes for which function compute() is known to be always below this value can be discarded.

Download:  SPALTER Source Code