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, a new method for loop invariant generation was introduced, which used the saturation and symbol elimination capabilities of Vampire to generate invariants containing quantifier alternations over programs with arrays, without any need for user guidance. The same technique has been extended to take into account pre and post-conditions of a loop; they can be used to filter the relevant invariants, but also to directly verify the partial correctness of the loop. This procedure offers an incomplete but automatic alternative to the classic Hoare rule for loops or its equivalent in other deductive systems.

Rather than being limited to a specific programming language, the implementation relies on a simple guarded command language for its input. We demonstrate how this representation can be used as an interface for more complex and realistic imperative languages, by integrating our tool in the KeY verification system, thus allowing automatic reasoning about loops in useful Java programs.

We will present the newly redesigned implementation of the loop reasoning feature in Vampire, its integration within KeY, as well as 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. The aim of the research reported on in this paper is to answer which SAT solver models are nice for the good performance of the AVATAR architecture. We establish criteria for which models should be preferred in theory, develop algorithmic ideas and heuristics on how to make the SAT solver produce models which satisfy these criteria, and experimentally evaluate the effectiveness of these ideas on the prover performance.

ABSTRACT. We present some of the new features of Vampire and make a proposal to include them in the TPTP standard.

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.