jMosel is a toolset for the analysis and verification in Monadic Second-Order Logic on Strings (M2L(Str)). It offers a decision procedure for M2L(Str) and is developed as the successor to the MoSeL tool-set using current technologies like Java and XML.
The emphasis is placed on flexibility to allow the customisation of nearly every aspect of the tool's properties. jMosel supports a variety of input and ouput formats including XML and DOT.
The syntax of jMosel offers means to intuitively formulate properties of bit vectors as well as set variables. Formulas are transformed into complete and deterministic finite-state automata in such a way that the language recognized by an automaton corresponds to the interpretation of the represented formula.
Currently there are two ways of accessing jMosel's functionality: several command line tools and a plugin to the jABC framework. The integration into the jABC enables the user to combine jMosel with other jABC components and thus to construct more sophisticated workflows.
The jMosel homepage can be found here.
jMosel is developed and maintained by Marco Bakera and Tiziana Margaria.