Automatic generation of loop invariants

The aim of this thesis is to develop a tool that is able to handle programs written in a subset of the C++ language and generate invariants automatically.
 

The field of invariant generation is based on a multitude of techniques such as computer algebra, theorem proving, constraint solving, abstract interpretation techniques or model-checking. Since reliable software design and implementation continues to be an important problem, any progress in this area will be extremely important in the future.

A particularly interesting case is the generation of loop invariants for programs or transition systems in general. In this context, an interesting method for automatically generate linear invariants, i.e. invariants expressed as a linear inequation, was presented by Colon, Sankaranarayanan and Sipma in 2003. This method uses Farkas Lemma to transform the problem of the existence of a loop invariant into a satisfiability problem in propositional logic over non-linear integral arithmetic. Despite the potential of the method, its application was limited due to the lack of good solvers for obtained non-linear constraints.

In this thesis, the new solver presented in Borralleras et al. 2011, which is able to deal with  arbitrary boolean formulas over non-linear inequations, will be used to solve the generated constraints.