Model checking Using Symbolic Execution

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

software

vyžadována - zdarma

Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Braione Pietro (DISCo, LTA)
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)

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/

European Research Training Network Segravis - Syntactis and Semantic Integration of Visual Modelling Techniques (HPRN-CT-2002-00275)
Metody a nástroje pro automatizované odhalování softwarových chyb (GP102/06/P076)
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů (GA102/07/0322)
Výzkum informačních technologií z hlediska bezpečnosti (MSM0021630528)

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

Universita degli Studi di Milano - Bicocca; Dipartimento di Informatica, Sistemistica e Comunicazione; Laboratory of Test and Analysis (DISCo, LTA)
Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)