ABSTRACT. This is a joint invited talk with the SMT 2019 workshop and will take place at the venue of the SMT 2019 workshop. 

ABSTRACT. Heuristics in theorem provers are often parameterised. Modern theorem provers such as Vampire (Kovács & Voronkov, 2013) utilise a wide array of heuristics to control the search space explosion, thereby requiring optimisation of a large set of parameters. An exhaustive search in this multi-dimensional parameter space is intractable in most cases, yet the performance of the provers is highly dependent on the parameter assignment. In this work, we introduce a principled probablistic framework for heuristics optimisation in theorem provers. We present results using a heuristic for premise selection integrated with Vampire and The Archive of Formal Proofs (AFP) (Jaskelioff & Merz, 2005) as a case study.

ABSTRACT. Demodulation is an important simplification rule in saturation-based theorem proving that performs rewriting using unit equalities.
However, in certain problem encodings, particularly ones coming from software verification, many useful equalities appear with side conditions.
We present (forward) subsumption demodulation, a generalization of demodulation to non-unit clauses,
and discuss its implementation in the theorem prover Vampire along with experimental results.

ABSTRACT. We are reporting on our ongoing efforts of providing Vampire within a Docker container that can run isolated from other instances in parallel. Testing the prover in different operating systems or with a particular runtime environment is now easier to automate. This also benefits attempts to rerun old experiments when the original binary has been lost. It also provides an excellent opportunity to run future experiments on a high-performance cluster.

ABSTRACT. The use of the AVATAR architecture within first-order theorem prover turns the work of the saturation core on a single monolithic problem into a sequence of simpler related sub-problems. We use the hints method for clause prioritisation to prefer selection of those clauses which already appeared in the proof of previous sub-problems. Based on the assumptions that the individual sub-problems tend to be related, this approach facilitates learning from past experience. In the talk I will describe the implementation of the idea in the automatic theorem prover Vampire and report on experimental results.

ABSTRACT. Automated program analysis and functional correctness verification require effective theory reasoning together with quantifiers in order to achieve full automation with efficiency.

In this work-in-progress presentation I would like to bring forward discussions with the Vampire development team on different design decisions for using Vampire in applications of program analysis. For example: Can we use (push) / (pop) SMT-statements to avoid axiom cluttering in verification condition generation? Some program transformations such as passification and single static assignments are particularly harmful to resolution provers, would it help if we limit the scope of such transformations? Should we use Vampire’s native support of theory of arrays or use type argumented axiomatization?

ABSTRACT. Many applications of theorem proving, for example program verification and analysis, require first-order reasoning with both quantifiers and theories such as arithmetic and datatypes. There is no complete procedure for reasoning in such theories but the state-of-the-art in automated theorem proving is still able to reason effectively with real-world problems from this rich domain. In this paper we introduce a missing part of the puzzle: automated induction inside a saturation-based theorem prover. Our goal is to incorporate lightweight automated induction in a way that complements the saturation-based approach, allowing us to solve problems requiring a combination of first-order reasoning, theory reasoning, and inductive reasoning. We implement a number of techniques and heuristics and evaluate them within the Vampire theorem prover. Our results show that these new techniques enjoy practical success on real-world problems.