Invariant generation in vampire

Kryštof Hoder; Laura Kovács; Andrei Voronkov

doi:10.1007/978-3-642-19835-9_7

Invariant generation in vampire

Kryštof Hoder, Laura Kovács, Andrei Voronkov

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

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. © 2011 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Pages	60-64
Number of pages	4
Volume	6605
DOIs	https://doi.org/10.1007/978-3-642-19835-9_7
Publication status	Published - 2011
Event	17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 - Saarbrucken Duration: 1 Jul 2011 → …

Conference

Conference	17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
City	Saarbrucken
Period	1/07/11 → …

Access to Document

10.1007/978-3-642-19835-9_7

Cite this

@inproceedings{793e53730f454891be16c739977d9eb2,

title = "Invariant generation in vampire",

abstract = "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. {\textcopyright} 2011 Springer-Verlag.",

author = "Kry{\v s}tof Hoder and Laura Kov{\'a}cs and Andrei Voronkov",

year = "2011",

doi = "10.1007/978-3-642-19835-9_7",

language = "English",

isbn = "9783642198342",

volume = "6605",

pages = "60--64",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

note = "17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 ; Conference date: 01-07-2011",

}

Hoder, K, Kovács, L & Voronkov, A 2011, Invariant generation in vampire. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 6605, pp. 60-64, 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrucken, 1/07/11. https://doi.org/10.1007/978-3-642-19835-9_7

TY - GEN

T1 - Invariant generation in vampire

AU - Hoder, Kryštof

AU - Kovács, Laura

AU - Voronkov, Andrei

PY - 2011

Y1 - 2011

N2 - 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. © 2011 Springer-Verlag.

AB - 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. © 2011 Springer-Verlag.

U2 - 10.1007/978-3-642-19835-9_7

DO - 10.1007/978-3-642-19835-9_7

M3 - Conference contribution

SN - 9783642198342

VL - 6605

SP - 60

EP - 64

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

T2 - 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011

Y2 - 1 July 2011

ER -

Invariant generation in vampire

Abstract

Conference

Access to Document

Fingerprint

Cite this