Efficient model checking using tabled resolution

Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David S. Warren

Research output: Chapter in Book/Report/Conference proceedingConference contribution

106 Scopus citations


We demonstrate the feasibility of using the XSB tabled logic programming system as a programmable fixed-point engine for implementing efficient local model checkers. In particular, we present XMC, an XSB-based local model checker for a CCS-like value-passing language and the alternation-free fragment of the modal mu-calculus. XMC is written in under 200 lines of XSB code, which constitute a declarative specification of CCS and the modal mu-calculus at the level of semantic equations. In order to gauge the performance of XMC as an algorithmic model checker, we conducted a series of benchmarking experiments designed to compare the performance of XMC with the local model checkers implemented in C/C++ in the Concurrency Factory and SPIN specification and verification environments. After applying certain newly developed logic-programming-based optimizations (along with some standard ones), XMC's performance became extremely competitive with that of the Factory and shows promise in its comparison with SPIN.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 9th International Conference, CAV 1997, Proceedings
EditorsOrna Grumberg
PublisherSpringer Verlag
Number of pages12
ISBN (Print)3540631666, 9783540631668
StatePublished - 1997
Externally publishedYes
Event9th International Conference on Computer-Aided Verification, CAV 1997 - Haifa, Israel
Duration: Jun 22 1997Jun 25 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th International Conference on Computer-Aided Verification, CAV 1997

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Efficient model checking using tabled resolution'. Together they form a unique fingerprint.

Cite this