C Program Bugs Analysis

The C language remains popular for the implementation of systems of the critical domain, where the consequences of errors are extremely costly. For the reliability of these systems, verification, and validation of C is very important. The motivation of this work is to use Frama-C for program analysis and verification.


Thesis Type:

  • IT-Project / Project / Seminar, B.Sc. Thesis, Master Thesis

Research Area:

  • Embedded Automotive System

Goal and Tasks:

  • Understanding of formal specification language ACSL
  • Explore different Frama-C analyzers.
  • Verification of different aspects of a C program using the Frama-C plugins.

Recommended Prior Knowledge:

  • C/C++ Programming
  • Computer architecture


  • As soon as possible.

Duration in months

  • 6 months (Master thesis)