author: Matthijs Hofstra
title: Loop invariant generation
keywords: invariant
topics: Logics and semantics
committee: Marieke Huisman
started: September 2017


In the literature, several approaches have been developed to generate loop invariants automatically. Strangely, program verification tools such as OpenJML, KeY etc., do not use these techniques; instead they require the specifier to add loop invariants manually.

Goal of this project is to investigate existing techniques for loop invariant generation, and to integrate them into an existing program verification tool.

The following steps will be necessary:

  • literature study into loop invariant generation and identification of what kind of problems can be handled with these techniques
  • integration of one or more promising techniques into a program verification tool
  • practical validation of the approach: are the generated loop invariants sufficient to prove correctness of the methods
  • possible extensions of the loop invariant generation techniques so that more programs can  be proven correct