Extensions

GSMC

GSMC is an experimental model checker for GSM, the Guard-Stage-Milestone language for programming artifact-centric systems. GSMC uses predicate abstraction techniques and is integrated with CVC4, one of the leading SMT solvers. GSMC is released as open-source and is developed as part of the ACSI (Artifact-centric Service Interoperations) EU FP7 research project.

Click here to download the source code: GSMC


MCMAS-P

MCMAS-P is an experimental model checker for the verification of multi-agent systems with an unbounded number of agents.

Click here to download the source code: MCMAS-P


MCMAS-S

MCMAS-S is an experimental model checker for the verification of security properties in unbounded multi-agent systems.

Click here to download the source code: MCMAS-S


MCMAS-SDD

MCMAS-SDD is an experimental SDD-based symbolic model checker for the verification of multi-agent systems.

Click here to download the source code: MCMAS-SDD


MCMAS-SLK

MCMAS-SLK is an experimental model checker for the verification of multi-agent systems against specifications given in epistemic strategy logic.

Click here to download the source code: MCMAS-SLK


MCMAS-SL[1G]

MCMAS-SL[1G] is an experimental model checker for the verification of multi-agent systems against specifications given in one-goal strategy logic.

Click here to download the source code: MCMAS-SL[1G]


MCMAS-LDLK

MCMAS-LDLK is an experimental model checker for the verification of multi-agent systems against specifications given in the logic LDLK.

Click here to download the source code: MCMAS-LDLK