The logically deep parts of the code are characterized by loops or recursions. For these parts, formal program verification is an appropriate tool. One of its biggest challenges is the automated discovery of auxiliary program assertions, leading to the discovery of safety and liveness properties of programs.
The increasing power of automated theorem proving and computer algebra have opened new perspectives for computer aided program verification, in particular for the automatic generation of invariant assertions and ranking functions in order to reason about loops and recursion. Especially promising breakthroughs are the assertion generation techniques by first-order theorem proving, satisfiability modulo theory (SMT) reasoning, and symbolic computation. These techniques can efficiently be used in conjunction with model checking, interpolation, static analysis and abstract interpretation.
We offer student projects (semester, master, PhD) dealing with the design of efficient methods for automated reasoning and generation of program assertions.
Project topics include, but are not limited to:
Contact: Laura Kovács.