For the first time in the history of the CADE ATP System Competition (CASC), a single automated theorem prover has achieved a clean sweep: VAMPIRE won all eight competition divisions at CASC-30. Even more remarkably, VAMPIRE solved more problems than all other competing systems combined, marking a historic milestone in automated reasoning. 

The VAMPIRE theorem prover is a computer program designed to prove logical statements automatically. It takes a set of known facts and logical rules and determines whether a new statement logically follows them. This makes it incredibly useful in software verification, mathematics, and artificial intelligence, where ensuring systems behave correctly and logically is critical. But as if winning all theorem proving divisions at CASC wasn't a big enough achievement, a paper about the development of VAMPIRE received the Distinguished Paper Award at the International Conference on Computer Aided Verification (CAV), one of the leading annual conferences on the theory and practice of computer-aided formal analysis of software and hardware systems. 

"These victories are not just individual achievements but a reflection of the collaborative strength of our entire research group at TU Wien Informatics, opens an external URL in a new window, working closely also with the University of Manchester, opens an external URL in a new window, the Czech Technical University in Prague,, opens an external URL in a new window and the University of Southampton, opens an external URL in a new window. This outcome underscores TU Wien's leading position in formal methods and the global impact of its research in automated reasoning.", notes Laura Kovács, Head of the Institute of Logic and Computation and the Research Unit Formal Methods in Systems Engineering, and one of the co-authors of the paper. 

The paper, The VAMPIRE Diary, opens an external URL in a new window, was written by Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdu, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov, and surveys the many changes that were developed and integrated in VAMPIRE in the past decade. Recent developments include improvements that help it understand and work with very complex types of logic, including those involving different objects, rules, and patterns. It also combines two powerful problem-solving methods, such as SAT/SMT solving to break problems into simpler ones, efficient reasoning with quantifiers, and the automation of induction.

"It was quite a long, but exciting journey - not just for continuous system development, but also in the consolidation of a really strong team of VAMPIRE developers.", reflects Laura Kovács. "Over the past years, TU Wien has become a stronghold for VAMPIRE development, but what is even more important to me is that we have a team of more than 12 highly determined experts to make VAMPIRE even stronger, pushing the boundaries of automated reasoning every day. It is simply fun and motivating, and we welcome new contributors!"

Congratulations to the team for winning the competition and to all the authors for this outstanding achievement! 

Curious about the paper? The paper is open-access and available to read or download on Springer Nature, opens an external URL in a new window.

A Vampire Diary Abstract

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 supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling VAMPIRE to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use VAMPIRE in practice and review the main changes VAMPIRE has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.