Fakulta informačních technologií VUT v Brně

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í
Nahoru