Record link: 
http://hdl.handle.net/20.500.12708/222596
-
Title: 
The Vampire Diary
en
Citation: 
Bártek, F., Bhayat, A., Coutelier, R., Hajdu, M., Hetzenberger, M., Hozzová, P., Kovács, L., Rath, J., Rawson, M., Reger, G., Suda, M., Schoisswohl, J., & Voronkov, A. (2025). The Vampire Diary. In R. Piskac & Zvonimir Rakamarić (Eds.), Computer Aided Verification (pp. 57–71). Springer. https://doi.org/10.1007/978-3-031-98682-6_4
-
Publisher DOI: 
10.1007/978-3-031-98682-6_4
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Bártek, Filip 
Bhayat, Ahmed 
Coutelier, Robin 
Hajdu, Márton 
Hetzenberger, Matthias 
Hozzová, Petra 
Kovács, Laura 
Rath, Jakob 
Rawson, Michael 
Reger, Giles 
Suda, Martin 
Schoisswohl, Johannes 
Voronkov, Andrei 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Computer Aided Verification 
-
ISBN: 
978-3-031-98682-6
-
Volume: 
15933
-
DOI of the book: 
10.1007/978-3-031-98682-6
-
Date (published): 
24-Sep-2025
-
Event name: 
37th International Conference Computer Aided Verification (CAV 2025) 
en
Event date: 
23-Jul-2025 - 25-Jul-2025
-
Event place: 
Zagreb, Croatia
-
Number of Pages: 
15
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
saturation-based theorem proving; Vampire; superposition calculus; AVATAR; Unification with Abstraction; inductive reasoning; program synthesis; higher-order theorem proving; FOOL; SAT/SMT solvers
en
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.
en
Project title: 
Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) 
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) 
LEARN: Learning Efficient Automated Reasoning on the Net: 101213411 (European Commission) 
QuAT: Quantifiers and Arithmetic Theories are Friends with Benefits: ARA 20223 (Amazon Research Awards) 
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) 
-
Project (external): 
TU Wien Doctoral College SecInt
CORESENSE
ERC CZ
ROBOPROX
-
Project ID: 
101070254
POSTMAN no. LL1902
CZ.02.01.01-00-22_008-0004590
-
Research Areas: 
Logic and Computation: 80%
Computer Science Foundations: 20%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

12
checked on Dec 16, 2025

Google ScholarTM

Check