15 citations · 25 across the 10 of their papers we have counts for
10 papers
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now…
Getting Saturated with Induction
Márton Hajdu, Petra Hozzová, Laura Kovács +2
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating indu…
To test, or not to test: A proactive approach for deciding complete performance test initiation
Omar Javed, Prashant Singh, Giles Reger +1
Software performance testing requires a set of inputs that exercise different sections of the code to identify performance issues. However, running tests on a large set of inputs c…
Boldly Going Where No Prover Has Gone Before
Giles Reger
I argue that the most interesting goal facing researchers in automated reasoning is being able to solve problems that cannot currently be solved by existing tools and methods. This…
Specification of State and Time Constraints for Runtime Verification of Functions
Joshua Heneage Dawes, Giles Reger
Techniques for runtime verification often utilise specification languages that are (i) reasonably expressive, and (ii) relatively abstract (i.e. they operate on a level of abstract…
A Story of Parametric Trace Slicing, Garbage and Static Analysis
Giles Reger
This paper presents a proposal (story) of how statically detecting unreachable objects (in Java) could be used to improve a particular runtime verification approach (for Java), nam…
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)
Giles Reger, Martin Suda, Andrei Voronkov
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover V…
Selecting the Selection
Giles Reger, Martin Suda, Andrei Voronkov +1
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implement…
Finding Finite Models in Multi-Sorted First Order Logic
Giles Reger, Martin Suda, Andrei Voronkov
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and en…
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger +1
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arr…