Tool homepage: http://www.tcs.hut.fi/Software/maria/
Tool availability: Free of charge
Maria is a reachability analyzer and a model checker whose modelling formalism is based on Algebraic System Nets, capable of handling tens of millions of reachable states and enabled transitions.
Maria includes a distributed algorithm for checking safety properties. The algorithm can be executed on multi-processor computers as well as on workstations in TCP/IP networks.
Optionally, nets can be unfolded or translated to transition systems.
Thanks to its modular design and open source license (GPL), Maria can easily be extended with new algorithms.
Marko M„kel„ Timo Latvala Laboratory for Theoretical Computer Science P.O.Box 5400 02015 Helsinki University of Technology Finland Phone: +358 - 9 - 451 2895 Fax: +358 - 9 - 451 3369 E-mail: email@example.com
Maria is efficient both in interactive use and in exhaustive reachability analysis, as it can both interpret models directly and compile them to fast C code.
The graphical user interface of Maria is based on GraphViz.