Sciweavers

Share
CADE
2007
Springer

Inferring Invariants by Symbolic Execution

10 years 10 months ago
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.
Benjamin Weiß, Peter H. Schmitt
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Benjamin Weiß, Peter H. Schmitt
Comments (0)
books