Page sem2009/abstracts/mine

Antoine Miné ENS, Paris

Title: Static analysis of run-time errors in parallel embedded C code

Abstract:

Astrée is a static analysis tool based on abstract interpretation that was developed at the ENS to prove the absence of run-time errors (such as arithmetic overflows or buffer overruns) in embedded critical avionics codes in C (without recursivity, dynamic memory allocation, nor parallelism).

We will present work-in-progress in developing a similar analyzer for embedded C codes featuring several concurrent processes communicating through shared memory and classic synchronisation mechanisms (without dynamic creation of processes nor synchronisation objects). In order to obtain an efficient analysis, our method abstracts away most of the inter-process control-flow information. It then reduces to a fixpoint computation where, at each step, each process is analyzed with respect to a mostly flow-insensitive abstraction of the effects of all other processes on it, and updates an abstraction of the effects it can have on others.

Early experimental results show that this method scales up to an actual industrial software comprising hundreds of thousands of C lines and a dozen of processes, although it generates many false alarms and much work is still needed to prove the absence errors fully automatically.