Detail produktu

Model checking Using Symbolic Execution

Vznik: 2008

Název česky
MUSE - model checking s využitím symbolického provádění
Typ
software
Licence
vyžadována - zdarma
Autoři
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Braione Pietro (DISCo, LTA)
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)
Popis

MUSE je prototypově implementovaný nástroj pro verifikaci Java programů, který pro popis ověřovaných vlastností přijímá formule lineární temporální logiky (LTL) a který využívá symbolické provádění Java bytekódu pro omezení problému stavové exploze.

Umístění
Projekty
Výzkumné skupiny
Pracoviště
Nahoru