Faculty of Information Technology, BUT

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
Back to top