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
Start:
Duration in months
Contact: