Inferring Invariants by Symbolic Execution

In this paper we propose a method for inferring invariants for loops in Java programs. An example of a simple while loop is used throughout the paper to explain our approach. The method is based on a combination of symbolic execution uting fixed points via predicate abstraction. It reuses the axiomatisation of the Java semantics of the KeY system. The method has been implemented within the KeY system which allows to infer invariants and perform verification within the same environment. We present in detail the results of a non-trivial example.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Benjamin Weiß, Peter H. Schmitt
• Keywords: Automated Reasoning, CADE 2007, Java Semantics, Non-trivial Example, Predicate Abstraction