jMosel is a new tool-set 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.

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.