Current Work

We have been working on the framework described in this diagram:

-  We have developed an extension to the GeneAuto platform, a Simulink to C compiler that is able to 
transfer stability information from Simulink to C, using new custom blocks at the Simulink level and custom 
symbols from the ACSL annotation language at the C level.

-  From there we have come up with a path to prove the correctness of the annotations in  PVS thanks to 
a linear algebra library.

-  The IKOS platform provides a modular way of writing abstract interpreters in order to  analyze the 
generated code for code specific issues. In particular one interpreter was  used to look for array bound
errors and performed considerably better than available commercial tools.