In Greek mythology, Urania was able to foretell the future by the possition of the stars.
In the computer age, MUSE is able to foretell the future faults by the Java byte-code.

1. Introduction
2. Requirements
3. Download
4. Installation
5. Tool execution
6. Related projects
7. Authors
8. Acknowledgement

1. P. Braione, G. Denaro, M. Pezze, and B. Krena: Verifying LTL Properties of Bytecode with Symbolic Execution, Bytecode 2008, [pdf]

1. Java SE Development Kit 6
2. Eclipse IDE for Java Developers - in principle, MUSE can be compiled and executed without Eclipse, however, we encountered some problems under the command line.
3. GNU C/C++ compiler g++ and make - we assume that they are already present under any reasonable UNIX/Linux evnironment while they can be installed under MS Windows operating systems through Cygwin - a Linux-like environment for Windows.
4. SICStus Prolog or CVC3 is used for expression simplification which is not essential part of symbolic execution, however, it usually leads to a significant reduction of state space provided by symbolic execution. Unfortunately, SICStus Prolog is not available free of charge while CVC3 makes symbolic execution very slow.
5. Spin or LTL2BA serves for translating LTL formulae to Büchi automata.
6. JavaCC™ - Java Compiler Compiler™ is used for building a translator from Büchi automata to Java source code.

1. Install all the required tools listed in the Requirements section.
   • When do you install Cygwin, please note that neither gcc nor make is a part of default Cygwin installation, however, the corresponding packages need to be selected within the Cygwin setup manually.
   • Path to executable files of installed tools (e.g., spin, JavaCC) can be set under MS Windows XP operating system in Control Panels (Ovládací panely), System (Systém), Details (Upřesnit), and Environment Variables (Proměnné prostředí). (I am not sure about the English names. I should check it under English Windows later.)
2. Download and expand the zip file(s) provided in the Download section.
3. Check the path setting in muse/scripts/set_environment.bat and execute it or use it for inspiration for path settings in your environment when the batch does not work properly in your operating system.
4. When do you want to use SICStus prolog for expression simplification make sure that you have downloaded and expanded SICStus interface and use usual command make (or make clean for cleaning) in the SicstusInterface directory. You will obtain SIIF.exe executable file that should be used for starting SICStus prolog engine before the MUSE tool.

never {    /* <> ( ap0 || ap1 ) */
T0_init:
	if
		:: ((((ap0)) || ((ap1)))) -> goto accept_all
		:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

• Symbolic execution extension of Java PathFinder
• Bogor/Kiasan

Institutions:

1. Laboratory of Test and Analysis, Dipartimento di Informatica Sistemistica e Comunicazion, Universita degli Studi di Milano - Bicocca, Italy
2. Faculty of Informatics, University of Lugano, Switzerland
3. Faculty of Information Technology, Brno University of Technology, Czech Republic

• the European Community through the European Research Training Network SegraVis, Contract Number HPRN-CT-2002-00275,
• the Czech Ministry of Education, Youth and Sports under the project Security-Oriented Research in Information Technology, Contract Number MSM0021630528,
• the Czech Science Foundation under the projects Advanced Formal Approaches in the Design and Verification of Computer-Based Systems, Contract Number GA102/07/0322 and Methods and Tools for Automated Bug Detection in Software, Contract Number GP102/06/P076.