Applied result detail

Model checking Using Symbolic Execution

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

Original Title

Model checking Using Symbolic Execution

English Title

Model checking Using Symbolic Execution

Type

Software

Abstract

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.

Abstract in English

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.

Keywords

Symbolic execution, code-based model checking of software.

Key words in English

Symbolic execution, code-based model checking of software.

Location

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

Licence fee

In order to use the result by another entity, it is always necessary to acquire a license

www

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