Identifikátory výsledku
Kód výsledku v 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>
Nalezeny alternativní kódy
RIV/68407700:21730/22:00370059 RIV/68407700:21730/23:00373789
Výsledek na webu
<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
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Vampire
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Vampire
Popis výsledku anglicky
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.
Klasifikace
Druh
R - Software
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA24-12759S" target="_blank" >GA24-12759S: Tvárné architektury pro automatické dokazování vět</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2025
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Interní identifikační kód produktu
Version 5.0
Technické parametry
https://github.com/vprover/vampire/releases/tag/v5.0.0
Ekonomické parametry
30%
IČO vlastníka výsledku
68407700
Název vlastníka
České vysoké učení technické v Praze, CIIRC