Title: ATL Verification for multi-agent systems In the first part of this talk, I'll give an overview of MCMAS, a model checker for multi-agent systems, introducing the semantics model, the input language and various features of MCMAS. The second part is devoted to verification of ATL formulae. Particularly, I'll talk about the generation of a single witness execution and all witness executions, as well as the counterexample when an ATL formula is not satisfied. A demo will be shown during the presentation.