Efficient Model Checking Using Tabled Resolution

10 years 6 months ago
Efficient Model Checking Using Tabled Resolution
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 XSBbased 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-programmingbased optimizations (along with some standard ones), XMC's performance became extremely competitive with that of the Factory and shows promise in its co...
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramak
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1997
Where CAV
Authors Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren
Comments (0)