<div class="csl-bib-body">
<div class="csl-entry">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.), <i>Computer Aided Verification</i> (pp. 57–71). Springer. https://doi.org/10.1007/978-3-031-98682-6_4</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/222596
-
dc.description.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
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
Amazon Research Awards
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
saturation-based theorem proving
en
dc.subject
Vampire
en
dc.subject
superposition calculus
en
dc.subject
AVATAR
en
dc.subject
Unification with Abstraction
en
dc.subject
inductive reasoning
en
dc.subject
program synthesis
en
dc.subject
higher-order theorem proving
en
dc.subject
FOOL
en
dc.subject
SAT/SMT solvers
en
dc.title
The Vampire Diary
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.editoraffiliation
Computer Science - Yale University (New Haven, US)
-
dc.relation.isbn
978-3-031-98682-6
-
dc.relation.doi
10.1007/978-3-031-98682-6
-
dc.relation.issn
0302-9743
-
dc.description.startpage
57
-
dc.description.endpage
71
-
dc.relation.grantno
ICT22-007
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
101213411
-
dc.relation.grantno
ARA 20223
-
dc.relation.grantno
F 8500
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Computer Aided Verification
-
tuw.container.volume
15933
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science (LNCS, Vol. 15933)
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.project.title
Effective Formal Methods for Smart-Contract Certification
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
LEARN: Learning Efficient Automated Reasoning on the Net
-
tuw.project.title
QuAT: Quantifiers and Arithmetic Theories are Friends with Benefits
-
tuw.project.title
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
80
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-031-98682-6_4
-
dc.description.numberOfPages
15
-
tuw.author.orcid
0000-0002-1822-2651
-
tuw.author.orcid
0000-0002-1343-5084
-
tuw.author.orcid
0009-0002-4735-5215
-
tuw.author.orcid
0000-0002-8273-2613
-
tuw.author.orcid
0000-0002-2052-8772
-
tuw.author.orcid
0000-0003-0845-5811
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.author.orcid
0000-0003-0346-6749
-
tuw.author.orcid
0000-0001-7834-1567
-
tuw.author.orcid
0000-0001-6353-952X
-
tuw.author.orcid
0000-0001-6990-8699
-
tuw.author.orcid
0000-0001-5550-196X
-
tuw.author.orcid
0000-0003-1073-7615
-
tuw.editor.orcid
0000-0002-3267-0776
-
tuw.editor.orcid
0000-0001-7946-0162
-
tuw.event.name
37th International Conference Computer Aided Verification (CAV 2025)
en
dc.description.sponsorshipexternal
TU Wien Doctoral College SecInt
-
dc.description.sponsorshipexternal
CORESENSE
-
dc.description.sponsorshipexternal
ERC CZ
-
dc.description.sponsorshipexternal
ROBOPROX
-
dc.relation.grantnoexternal
101070254
-
dc.relation.grantnoexternal
POSTMAN no. LL1902
-
dc.relation.grantnoexternal
CZ.02.01.01-00-22_008-0004590
-
tuw.event.startdate
23-07-2025
-
tuw.event.enddate
25-07-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Zagreb
-
tuw.event.country
HR
-
tuw.event.presenter
Rawson, Michael
-
tuw.event.track
Multi Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.cerifentitytype
Publications
-
item.fulltext
no Fulltext
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
none
-
item.openairetype
conference paper
-
item.languageiso639-1
en
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0000-0002-1822-2651
-
crisitem.author.orcid
0000-0002-1343-5084
-
crisitem.author.orcid
0009-0002-4735-5215
-
crisitem.author.orcid
0000-0002-8273-2613
-
crisitem.author.orcid
0000-0002-2052-8772
-
crisitem.author.orcid
0000-0003-0845-5811
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.orcid
0000-0003-0346-6749
-
crisitem.author.orcid
0000-0001-7834-1567
-
crisitem.author.orcid
0000-0001-6353-952X
-
crisitem.author.orcid
0000-0001-6990-8699
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
