The Vampire Diary

• Published in 2025
• Added on 2025-06-18

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.

Links

• http://arxiv.org/abs/2506.03030v1
• http://arxiv.org/pdf/2506.03030v1

Other information

BibTeX entry

@article{TheVampireDiary,
	key = {TheVampireDiary},
	type = {article},
	title = {The Vampire Diary},
	author = {Filip B{\'{a}}rtek and Ahmed Bhayat and Robin Coutelier and M{\'{a}}rton Hajdu and Matthias Hetzenberger and Petra Hozzov{\'{a}} and Laura Kov{\'{a}}cs and Jakob Rath and Michael Rawson and Giles Reger and Martin Suda and Johannes Schoisswohl and Andrei Voronkov},
	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.},
	comment = {},
	date_added = {2025-06-18},
	date_published = {2025-06-18},
	urls = {http://arxiv.org/abs/2506.03030v1,http://arxiv.org/pdf/2506.03030v1},
	collections = {attention-grabbing-titles,basically-computer-science},
	url = {http://arxiv.org/abs/2506.03030v1 http://arxiv.org/pdf/2506.03030v1},
	year = 2025,
	urldate = {2025-06-18},
	archivePrefix = {arXiv},
	eprint = {2506.03030},
	primaryClass = {cs.LO}
}