Model checking Using Symbolic Execution

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

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

Projects

Advanced Formal Approaches in the Design and Verification of Computer-Based Systems (GA102/07/0322)
European Research Training Network Segravis - Syntactis and Semantic Integration of Visual Modelling Techniques (HPRN-CT-2002-00275)
Methods and Tools for Automated Bug Detection in Software (GP102/06/P076)
Security-Oriented Research in Information Technology (MSM0021630528)

Research groups

Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)

Departments

Department of Intelligent Systems FIT BUT (DITS FIT BUT)
Universita degli Studi di Milano - Bicocca; Dipartimento di Informatica, Sistemistica e Comunicazione; Laboratory of Test and Analysis (DISCo, LTA)