Automated Generation of Loop Invariants for Program Verification
The logically deep parts of the code are characterized by
(possibly nested) loops or recursions. For these parts,
formal program verification is an appropriate tool.
One of its biggest challenges is the automated discovery
of inductive assertions, leading to the discovery of safety and
security 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 inductive assertions
in order to reason about loops and recursion.
Especially promising breakthroughs are the invariant
generation techniques by polynomial algebra, quantifier
elimination, and algorithmic combinatorics, which can
be used in conjunction with model checking, theorem
proving, static analysis and abstract interpretation.
We offer semester or master projects dealing with the design of efficient and automatic methods for
The project topics could be:
case studies/experimental evaluations using available methods for the generation of loop invariants. Improvements (and if possible, extensions) on the existing algorithms for invariant generation are highly welcomed;
- design and implementation of automated invariant generation methods for relatively complex programs
over common data structures such as arrays, strings and pointers.