DiVinE Cluster
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00024473" target="_blank" >RIV/00216224:14330/08:00024473 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
DiVinE Cluster
Original language description
New generation of DiVinE -- parallel LTL model checker. The major extensions include * Limited support for ProMeLa modelling language. * Improved scalability (up to hundreds of cores). * Improved model interpretation and pre-compilation subroutines.
Czech name
DiVinE Cluster
Czech description
Nová generace nástroje DiVinE. Rozšiřující předchozí LTL Model Checker DiVinE. Významná rozšíření jsou zejména tato: * Částečná podpora modelovacího jazyka ProMeLa. * Rošíření škálovatelnosti a to na platformy o řádově větším počtu uzlů (stovky jader). *Akcelerace verifikačního procesu nahrazením interpretace modelů kompilovanou formou.
Classification
Type
R - Software
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2008
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
divine-cluster
Technical parameters
LTL model checker využívající agregované výpočetní síly uzlů v klastru. Nástroj využívá rozhraní MPI. Verze 0.8.2.
Economical parameters
—
Owner IČO
00216224
Owner name
Masarykova univerzita