MCMAS is an OBDD-based symbolic model checker tailored to the verification of Multi-Agent Systems (MAS). MAS descriptions are given by means of programs in ISPL (Interpreted Systems Programming Language), a modular language inspired by interpreted systems, a popular semantics in MAS.

MAS supports a rich set of specifications, including CTL operators, epistemic operators, ATL, and  notions pertaining to correct behaviour. Basic fairness conditions are supported. MCMAS produces counterexamples and witness executions for a wide range of specifications.

In addition to stand-alone mode a graphical interface (based on Eclipse) supporting a wide range of features is provided.