Product Details

Model checking Using Symbolic Execution

Created: 2008

Czech title
MUSE - model checking s využitím symbolického provádění
Type
software
License
required - free
Authors
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT)
Braione Pietro (DISCo, LTA)
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)
Keywords

Symbolic execution, code-based model checking of software.

Description

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.

Location
Projects
Research groups
Departments
Back to top