Vampire 2014 and 2015: Papers with Abstracts

Abstract. Sledgehammer integrates third-party automatic theorem provers in the proof
assistant Isabelle/HOL. In the seven years since its first release in 2007, it
has grown to become an essential part of most Isabelle users' workflow. Although
a lot of work has gone into tuning the system, the main reason for
Sledgehammer's success is the impressive power of the external provers,
especially E, SPASS, Vampire, and Z3. In this paper, I review
Vampire's strengths and weaknesses in this context and propose a few
directions for future work.

Abstract. The Vampire ATP system has been very successful at proving theorems in
first-order logic.
Vampire has won the FOF division of CASC for all except one of the last 15
years, and many papers highlighting Vampire's strengths have been published.
This talk examines the flip side of the Vampire coin ... what kinds of
problems are difficult or even impossible for the latest incarnation of
Vampire.
The talk will help users decide when to use Vampire, and when to use another
ATP system, will help the Vampire developers direct their work, and provides
the data required to build a portfolio ATP system with Vampire as a component.

Abstract. In order to better understand how well a state of the art SAT solver would behave in the framework of a first-order automated theorem prover we have decided to integrate Lingeling, best performing SAT solver, inside Vampire’s AVATAR framework. In this paper we propose two ways of integrating a SAT solver inside of Vampire and evaluate overall performance of this combination. Our experiments show that by using a state of the art SAT solver in Vampire we manage to solve more problems. Surprisingly though, there are cases where combination of the two solvers does not always prove to generate best results.

Abstract. Type systems for programming languages shall detect type errors in programs before runtime. To ensure that a type system meets this requirement, its soundness must be formally verified. We aim at automating soundness proofs of type systems to facilitate the development of sound type systems for domain-specific languages.
Soundness proofs for type systems typically require induction. However, many of the proofs of individual induction cases only require first-order reasoning. For the development of our workbench Veritas, we build on this observation by combining automated first-order theorem provers such as Vampire with automated proof strategies specific to type systems. In this paper, we describe how we encode type soundness proofs in first-order logic using TPTP. We show how we use Vampire to prove the soundness of type systems for the simply-typed lambda calculus and for parts of a typed SQL. We report on which parts of the proofs are handled well by Vampire, and what parts work less well with our current approach.

Abstract. In 2009, the symbol elimination method for loop invariant generation
was introduced, which used saturation
theorem proving in first-order logic to generate quantified invariants
of programs with arrays. Symbol elimination is fully automatic,
requires no user guidance, and it is the first ever approach able to
generate invariants with alternations of quantifiers. In this paper
we describe a number of improvements and extensions to symbol
elimination and invariant generation using first-order theorem
proving, in particular the Vampire theorem prover. Rather than being
limited to a specific programming language, our approach to reasoning
about loops in Vampire relies on a simple guarded command language for
its input, which can be used as an interface for more complex and
realistic imperative languages. We propose new ways for extending
quantified loop properties describing valid loop properties, by
simplifying the properties over array updates and next state
relations. We also extend symbol elimination with pre- and
post-conditions of loops. We use the loop specification to generate
only invariants that are relevant, that is, invariants that are needed
for proving partial correctness of loops. Further, we turn symbol
elimination into an automatic approach proving program correctness,
providing an alternative method to Hoare-rule based loop verification
or other deductive systems. We present our newly redesigned
implementation of loop reasoning in Vampire and also report on
experimental results.

Abstract. Reasoning in a saturation-based first-order theorem prover is generally expensive involving complex term-indexing data structures and inferences such as subsumption resolution whose (worst case) running time is exponential in the length of the clause. In contrast, SAT solvers are very cheap, being able to solve large problems quickly and with relatively little memory overhead.
Consequently, utilising this cheap power within Vampire to carry out certain tasks has proven highly successful. We give an overview of the different ways that SAT solvers are utilised
within Vampire and discuss further ways in which this usage could be extended

Abstract. This paper presents and explores experimental results examining the usage of AVATAR (Advanced Vampire Architecture for Theories and Resolution). This architecture introduces a new method for splitting in first-order resolution and superposition theorem provers that makes use of a SAT (or SMT) solver to make splitting decisions. The architecture (as implemented in Vampire) has many options and components that can be varied and this paper explores the effects of these variations on the performance of the prover.