First-Order Theorem Proving with Vampire

The first version of the Vampire theorem prover was implemented 20 years ago, in 1994. Vampire has always been known for its fast and efficient implementation, for example it has won 30 world cup winner titles in first-order theorem proving.

In this talk we will first briefly overview the history of Vampire. Next, we address current results and trends in Vampire, with special focus on applications of reasoning in program analysis and verification. The current version of Vampire is faster than any of its previous versions and includes several new, non-standard features such as SAT/SMT solving, reasoning with theories, program analysis, consequence elimination, invariant generation, interpolation, and reasoning with very large theories.