Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
K. Hoder, L. Kovacs, A. Voronkov:
"Invariant Generation in Vampire";
Vortrag: 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Saarbrücken;
26.03.2011
- 03.04.2011; in: "Proc. of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
Springer,
LNCS 6605
(2011),
ISBN: 978-3-642-19834-2;
S. 60
- 64.
Kurzfassung deutsch:
This paper describes a loop invariant generator implemented in the theorem prover Vampire. It is based on the symbol elimination method proposed by two authors of this paper. The generator accepts a program written in a subset of C, finds loops in it, analyses the loops, generates and outputs invariants. It also uses a special consequence removal mode added to Vampire to remove invariants implied by other invariants. The generator is implemented as a standalone tool, thus no knowledge of theorem proving is required from its users.
Kurzfassung englisch:
This paper describes a loop invariant generator implemented in the theorem prover Vampire. It is based on the symbol elimination method proposed by two authors of this paper. The generator accepts a program written in a subset of C, finds loops in it, analyses the loops, generates and outputs invariants. It also uses a special consequence removal mode added to Vampire to remove invariants implied by other invariants. The generator is implemented as a standalone tool, thus no knowledge of theorem proving is required from its users.
Schlagworte:
program verification, loop invariants, interpolants, theorem proving
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_205717.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.