WP3: Combining Static Analyses Techniques

Frama-C is a collaborative framework for static analysis techniques that has been implemented during the CAT project. This work package is dedicated to the study of some possible promising combinations between such techniques or variation of such techniques.

In particular, the collaboration between abstract interpretation and weakest-precondition computation will be extensively studied and implemented. Slicing and impact analysis techniques will also be combined with weakest-precondition computation in order to specialise the source code according to specific properties. This will eventually ease or even make possible a deductive proof by removing spurious C constructs that could impair the precondition computation in a correct automatic manner.

Different kinds of source code require heterogeneous levels of abstractions for weakest-precondition computations. Therefore proper memory models must be defined and be combined in order to cope with large source code.

To improve abstract interpretation in itself, the collaboration between non relational and numerical relational lattices will be implemented in a generic way.

This work package will in particular take into account the results of WP1 (Floating Point Analysis) and WP2 (Temporal Properties). In addition, like these two work packages, an efficient collaboration between the analyzers will lower the cost of static analysis and thus help its dissemination, as planned in WP6 (Spreading Static Analysis). Last, the formalisation effort of WP5 (Trusting Formal Methods) will be primarily based on the models and abstractions devised during WP3.