The Vampire Diary
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908496105046016 |
|---|---|
| author | 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 |
| author_facet | 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 |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_03030 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Vampire Diary 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 Logic in Computer Science 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. |
| title | The Vampire Diary |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.03030 |