|title:||Loop invariant generation|
|topics:||Logics and semantics|
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