Download XMC

XMC is a model checker implemented using the XSB tabled logic programming system. XMC is an explicit-state, local model checker for processes specified in XL, a sugared version of value-passing CCS, and the alternation-free fragment of the modal mu-calculus. The XMC system is a result of the LMC (Logic-Programming-Based Model Checking) project at Stony Brook.

XMC v1.1.2 is now available in the following format:

See README for terms of use.

System Requirements for v1.1.2:

XMC can be used in text-only (non-graphical) mode; if this is all you are interested in, then installing XSB is sufficient to run XMC.

If you have any problems downloading, installing, or running XMC, please send mail to with a short description of the problem and the platform (OS, XSB version) you are operating on.

Last modified: Mon Dec 17 12:26:09 EST 2001