@inproceedings{14ab7181227b4d5983e10b276c1561d4,
title = "Efficient model checking using tabled resolution",
abstract = "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.",
author = "Ramakrishna, {Y. S.} and Ramakrishnan, {C. R.} and Ramakrishnan, {I. V.} and Smolka, {Scott A.} and Terrance Swift and Warren, {David S.}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 9th International Conference on Computer-Aided Verification, CAV 1997 ; Conference date: 22-06-1997 Through 25-06-1997",
year = "1997",
doi = "10.1007/3-540-63166-6_16",
language = "English (US)",
isbn = "3540631666",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "143--154",
editor = "Orna Grumberg",
booktitle = "Computer Aided Verification - 9th International Conference, CAV 1997, Proceedings",
}