Model checking Using Symbolic Execution

Název česky

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

Typ

software

Licence

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

Licenční poplatek

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

Autoři

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

Klíčová slova

Symbolic execution, code-based model checking of software.

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í

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

Projekty

Metody a nástroje pro automatizované odhalování softwarových chyb, GAČR, Postdoktorandské granty, GP102/06/P076, zahájení: 2006-01-01, ukončení: 2008-12-31, 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, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení

Výzkumné skupiny

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

Pracoviště

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