ABSTRACT. I will present the model-constructing (MCSAT) approach to solving satisfiability modulo theory (SMT) problems, with a focus on recent developments. MCSAT is a model-driven reasoning framework for SMT that generalizes modern CDCL-style SAT solvers to first-order setting. It is a competitive alternative to the standard DPLL(T) approach with many appealing features: simplicity, deductive power, extensibility, and effectiveness on real-world problems. Going beyond the core SMT problem, I will also discuss how model-driven reasoning can provide an alternate route for challenging tasks such as interpolation, generalization, and quantified reasoning.

ABSTRACT. Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.

ABSTRACT. In our ongoing project VeriTaS, we aim at automating soundness proofs for type systems of domain-specific languages. In the past, we successfully used previous Vampire versions for automatically discharging many intermediate proof obligations of standard soundness proofs for small type systems. However, so far, encoding the individual proof problems required manual encoding of algebraic datatypes via the theory of finite term algebras. One of the new Vampire versions now supports the direct specification of algebraic datatypes and integrates reasoning about term algebras into the internally used superposition calculus.

In this work, we investigate how well the new Vampire 4.1 version with support for algebraic datatypes performs within our type soundness case studies, compared to previous Vampire versions.

ABSTRACT. In order to prove functional correctness, program verification tools traditionally rely on satisfiability modulo theories (SMT) solvers to prove verification conditions. SMT solvers offer a powerful support for decidable theory-specific reasoning, but are more limited in dealing with quantified formulas – which weakens the robustness of the verification process and requires, on top of functional specifications, additional user annotations. In particular, to support quantifier reasoning, SMT solvers require users to guide variable instantiations using patterns known as triggers [2]. In this work, we propose to replace SMT solvers with first-order theorem provers to prove verification conditions. First-order provers can deal with quantification flexibly and without special annotations. In order to cater to a variety of verification tools, we target (a core subset of) the popular Boogie intermediate verification language [4], for which we provide an encoding of verification conditions in TPTP [5]. The encoding expressly takes advantage of the recent “FOOL”[3] extensions to the Vampire prover, which facilitate reasoning about the semantics of imperative constructs. Experiments with our blt tool [1], implementing the encoding, on a variety of Boogie programs suggest that first-order provers can help make functional verification robust and more applicable.

ABSTRACT. Both SMT and SAT solvers can be used incrementally. This can be useful in lots of applications. Indeed, internally, Vampire uses both Minisat and z3 incrementally. In this paper, we explore how Vampire can be used incrementally. There are two forms of incremental solving. The first is where a solver is provided with formulas from a problem one by one with consistency being checked at certain points. The second more general form is where stack operations are used to create different solving contexts. We explore both ideas and show how they can be achieved within Vampire. We argue that the second approach may be more suited to Vampire as it allows for the incremental solving of unsatisfiable problems (whereas the first assumes a series of satisfiable problems) and the use of different solving contexts allows Vampire to make use of incomplete proof search strategies. For the first approach, it is necessary to restrict preprocessing steps to ensure completeness when additional formulas are added. For the second approach, we make use of clauses labelled with assertions and take advantage of AVATAR to keep track of the stack information.

ABSTRACT. Modern large-scale cloud infrastructures are inherently complex. They often contain networks with thousands of nodes, intricate routing rules and security policies. Analysis of network configurations for such infrastructures is hard and requires specialised tools. Tiros is a static analyzer for Amazon Web Services (AWS) networks. Tiros takes the configuration of a network and answers queries about reachability of the nodes in the network. Examples of Tiros queries are "Is there a node that is reachable by SSH from the internet?" and "List all nodes that can be pinged from the node X". We present an implementation of a query engine for Tiros, based on automated theorem proving in first-order logic. This query engine translates the description of the network and the query into a first-order problem and uses Vampire to solve it. This work has been done during the author's visit to AWS.

ABSTRACT. One of the state-of-the-art approaches to generating first-order interpolants is based on processing so called local proofs and combining conclusions of color-eliminating inferences. Such an approach to interpolation can be stated in terms of assigning colors to the symbols of the signature and local proofs are those that do not mix colors in inferences. Local proofs can be obtained by instructing a first-order prover to block inferences that would violate this rule. Such a restriction in general does not preserve completeness, but local proofs are discovered in many cases.

One of the most influential improvements of first-order theorem provers of recent years is the AVATAR architecture for clause splitting. AVATAR employs a SAT solver to pick splitting branches, thus delegating the propositional essence of the given problem to the dedicated solver. This leads to a combination which has been shown to be highly successful in practice. However, the most straightforward adaptation of AVATAR to produce local proofs is quite restrictive as it does not allow the important color-eliminating inferences to happen within the first-order part of the prover.

In this paper, we explore how severely this restriction impairs the strength of AVATAR for finding local proofs in practice. We then propose and evaluate a new approach for obtaining local proofs with AVATAR which compromises on the side of clause splitting and the use of a SAT solver to allow first-order color-eliminating inferences in AVATAR.

ABSTRACT. Question answering is the process of taking a conjecture existentially quantified at the outermost level and providing one or more instantiations of these variables as a form of an answer to the implied question. For example, given the axioms p(a) and f(a)=a the question ?[X] : p(f(X)) should return the answer X=a. This paper reviews the question answering problem, describes how it is tackled within the Vampire theorem prover, and discusses new additions including the ability to answer questions involving arithmetic and the integration with finite model finding.