A Property-Driven Approach Towards a Loop Invariant Generator in KeY Using Symbolic Execution

Abstract

Software verification is the field of study that concerns itself with proving the correctness of a computation system formally. Hereby, the prover is given a precondition that it assumes to be true at the start of the system and a postcondition that has to be proved using the precondition and the system. In the absence of unbounded loops, jumps or recursion, formally proving that some property holds is possible in a finite amount of time. In order to make assertions about unbounded loops a loop invariant is needed, that holds inductively in each loop iteration and is strong enough to prove the safety assertion of the program. Finding loop invariants is tedious to do manually, which is why automatic techniques for loop invariant generation have been a subject of research since the 1960s. The software verification tool KeY is missing a loop invariant generator, which is implemented over the course of this thesis project. The invariant generator employs property-driven solutions to infer loop invariants using verification conditions that are generated using the symbolic execution engine of the KeY project. The generator is able to infer loop invariants for some simple loops over integer scalar and array variables.