Abstraction On-Demand: Automatically Generating Invariants for Loops and Recursive Method Calls

As a part of the RiSE seminar series, the Institute of Information Systems hosted a talk by Nathan Wasser.

ABSTRACT

Finding useful, i.e., sufficiently precise, invariants for loops and recursive method calls is a challenging task, even for skilled professionals. Automatically generating such invariants is an even more daunting task. However, this automation can be extremely useful and even unsuccessful attempts can give insight into where refinements must be made, simplifying and shortening the work which must be done manually.

An extension to the verification tool KeY allows the automatic generation of such invariants. In order to ensure termination, this approach is based on abstractions. However, rather than abstracting the program itself, the symbolic state of the program generated by symbolic execution is abstracted on demand only when dealing with loops or recursion. This allows high precision to be kept whenever possible.

The theoretical framework will be discussed, in particular abstrations for both loops and recursive calls, as well as abstraction mechanisms for array accesses. The tool will be demonstrated, showing at least each of these aspects and more if time is available.