Development of a Verification Compiler for C Programs

OData support
Supervisor:
Tóth Tamás
Department of Measurement and Information Systems

As embedded systems are becoming more and more common in our lives, the importance of their safe and fault-free operation is becoming even more critical.

Unlike testing, formal verification can not only prove the presence of errors, but their absence as well, making it suitable for verifying safety-critical systems.

Formal verification may be done by transforming the already implemented source code to a formal model and querying the resulting model's properties on the reachability of an erroneous state.

Sadly, source code to formal model transformations often yield unmanageably large and complex models, resulting in an extremely high computational time for the verifier. In this work I propose a complex workflow which provides a source code to formal model transformation, with program size reduction optimizations. These optimizations include constant propagation, dead branch elimination, loop unrolling, function inlining, extended with a program slicing algorithm which splits a single large problem into multiple smaller ones. At the end of the workflow, a bounded model checker and a k-induction algorithm verifies these smaller slices.

Furthermore, I provide benchmarks to demonstrate the usability and efficiency of this workflow and the effect of the optimization algorithms on the formal model.

Downloads

Please sign in to download the files of this thesis.