Model checking Using Symbolic Execution

MUSE - model checking s využitím symbolického provádění

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Křena Bohuslav, Ing., Ph.D. (UITS)
Braione Pietro
Denaro Giovanni
Pezze Mauro, prof.

Symbolic execution, code-based model checking of software.

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.

http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/

Metody a nástroje pro automatizované odhalování softwarových chyb, GAČR, Postdoktorandské granty, GP102/06/P076, 2006-2008, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, 2007-2009, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, řešení

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Ústav inteligentních systémů (UITS)