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
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
Authors
Křena Bohuslav, Ing., Ph.D. (DITS)
Braione Pietro
Denaro Giovanni
Pezze Mauro, prof.
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, GACR, Standardní projekty, GA102/07/0322, 2007-2009, completed
Methods and Tools for Automated Bug Detection in Software, GACR, Postdoktorandské granty, GP102/06/P076, 2006-2008, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top