Lecturer: Pascal Cuoq.
Frama-C is a framework for combining analysis techniques towards the analysis or verification of C code.
Why C? C is widely use for embedded programming. In a tiny number of cases, the embedded software is critical: lives depend on it functioning as expected. These applications do, and will increasingly, take advantage of formal methods.
Why combining techniques? Because each of them still has limitations on its own (in some cases, the limitation is intrinsic to the approach and will not be removed with any amount of research). In Frama-C, each technique, implemented as a plug-in, can complement the others, take advantage of the results they have computed, and provide its own results to other plug-ins.
In this course, we will explore the different plug-ins that have already been implemented within the framework.
Frama-C is available for download.
answerthat causes the problem to appear. Send your results, outlining very precisely what you did so that they can be reproduced, before 2010/07/07 at 12:00 to Pascal.Cuoq@gmail.com.
In order to take full advantage of this course, it is strongly recommended