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 invariant generation.

The project topics could be:
  1. 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;

  2. design and implementation of automated invariant generation methods for relatively complex programs over common data structures such as arrays, strings and pointers. 

Contact: Laura Kovács.