The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F25%3A00389184" target="_blank" >RIV/68407700:21730/25:00389184 - isvavai.cz</a>
Alternative codes found
RIV/68407700:21730/22:00370059 RIV/68407700:21730/23:00373789
Result on the web
<a href="https://github.com/vprover/vampire/releases/tag/v5.0.0" target="_blank" >https://github.com/vprover/vampire/releases/tag/v5.0.0</a>
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Vampire
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
R - Software
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA24-12759S" target="_blank" >GA24-12759S: Malleable Theorem Proving Architectures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Internal product ID
Version 5.0
Technical parameters
https://github.com/vprover/vampire/releases/tag/v5.0.0
Economical parameters
30%
Owner IČO
68407700
Owner name
České vysoké učení technické v Praze, CIIRC