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.
CITATION STYLE
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) (Vol. 6605 LNCS, pp. 60–64). https://doi.org/10.1007/978-3-642-19835-9_7
Mendeley helps you to discover research relevant for your work.