From SE Wiki
Revision as of 16:37, 22 December 2010 by (Talk)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search


XChek is a multi-valued symbolic model checker. It is a generalization of an existing symbolic model checking algorithm to an algorithm for amulti-valued extension of CTL (XCTL). Given a system and a XCTL property, XChek returns the degree to which the system satisfies the property.

The main features of Chek are the following:

  • Multi-valued logics: 2-valued, 3-valued, upset, 4-valued disagreements, etc. Users can define their own logics.
  • Multiple model formats: reads SMV and GCLang models. Multi-valued models are specified in XML.
  • Proof-like counterexamples: proof rules are used to generate counterexamples. Counterexamples can be generated statically or dynamically, and various viewers are available.

Website: XChek and user manual