Logik und Formale Methoden

Inferring Invariants by Symbolic Execution

  • Autor(en):

    Peter H. Schmitt
    Benjamin Weiß

  • Quelle:

    4th International Verification Workshop (VERIFY'07), Workshop at CADE-21, Bremen, Germany, 2007

  • 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 and computing 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.

BibTeX

@inproceedings{SchmittWeiss2007,
  author       = {Peter H. Schmitt and Benjamin Wei{\ss}},
  title        = {Inferring Invariants by Symbolic Execution},
  editor       = {Bernhard Beckert},
  booktitle    = {Proceedings, 4th International Verification Workshop (VERIFY'07)},
  volume       = {259},
  series       = {CEUR Workshop Proceedings},
  pages        = {195--210},
  publisher    = {CEUR-WS.org},
  year         = {2007}
}