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:
System Requirements for v1.1.2:
- XSB logic programming system v2.1 or higher. XSB runs on
various Unices, Windows 95/98 and NT. For acquiring and
installing XSB, please consult the official XSB home page.
- iTcl/Tk v3.0 or higher. Please see the
iTcl/Tk page for instructions
on downloading and installing this software. It is also available
as a RedHat RPM.
You can download the file itcl-3.*.rpm from one of the
RedHat Mirror Sites.
- The installation scripts provided with XMC v1.1.2 have been
tested only on Unix platforms.
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
If you have any problems downloading, installing, or running XMC,
please send mail to
firstname.lastname@example.org 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