Section: Software

Aoraï

Participant : Nicolas Stouls.

Developed at CEA-LIST, Frama-C is an extensible and collaborative platform dedicated to source-code analysis of C software. The Aoraï  [49] plug-in for Frama-C  [31] provides a method to automatically annotate a C program according to a behavioral property P such that, if the annotations are verified, then we ensure that the program respects P.

The computation process is divided into two steps: the specification generation from the property and the constraints propagation for static simplification. According to the classical invariant verification granularity, observable states of a program correspond to each call or return statements of an operation. Each state of the program is associated to a set of transitions in an internal representation of the property, managed as a Büchi automata. Starting from a super-set of authorized behaviors, some static simplifications can be done in order to generate sufficient pre/post-conditions on each operation.

The classical method to validate generated annotations is to use the Jessie plug-in and the Why tool, using theorem provers.

A new research report  [50] as been published and some new developments has been done in order to increase consequently the efficiency of the tool.