Detail aplikovaného výsledku

Model checking Using Symbolic Execution

KŘENA, B.; BRAIONE, P.; DENARO, G.; PEZZE, M.

Originální název

Model checking Using Symbolic Execution

Anglický název

Model checking Using Symbolic Execution

Druh

Software

Abstrakt

MUSE is a prototype implementation of a tool for verification of LTL properties against Java byte-code which uses symbolic execution technique for combatting the state space explosion problem.

Abstrakt aglicky

MUSE is a prototype implementation of a tool for verification of LTL properties against Java byte-code which uses symbolic execution technique for combatting the state space explosion problem.

Klíčová slova

Symbolic execution, code-based model checking of software.

Klíčová slova anglicky

Symbolic execution, code-based model checking of software.

Umístění

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

Licenční poplatek

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

www

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