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.
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.
Further informations about our approach can be found in:
WARNING: MUSE is a research prototype tool and not one-push-button solution. During its development, we have concentrated on the core ideas (e.g., symbolic execution, LTL model checking) much more than on the easy to use interface. We are sorry for the discomfort of the user, however, the intention of sharing the tool is not to provide ready-to-use tool but to share the ideas inside the tool and the effort already dedicated for its development with other researchers interested in using symbolic execution (not only) for model checking.
never { /* <> ( ap0 || ap1 ) */
T0_init:
if
:: ((((ap0)) || ((ap1)))) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}
which can be used (after some unnecessary brackets removing) as
the input of ba2j translator and then as the input of MCEngine.
After the translation, the Buchi automaton should be
checked and some unnecessary brackets can be removed.