XMC: A Logic-Programming-Based Verification Toolset

C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury, V. N. Venkatakrishnan


XMC supports the specification and verification of concurrent systems such as communication protocols and embedded systems. It is implemented atop XSB, a high-performance logic-programming system. System models are specified in XL, a typed value-passing language based on CCS, properties of interest are specified in the modal mu-calculus, and model checking is used to verify properties of systems. XMC incorporates a justifier which allows the user to navigate the proof tree underlying a model-checking computation; such proof trees are effective in debugging branching-time formulas. XMC has been successfully applied to the specification and verification of a variety of systems including the Rether real-time Ethernet protocol, the Java meta-locking algorithm, and the SET e-commerce protocol.

Bibtex Entry:

author = {C. R. Ramakrishnan and  I. V. Ramakrishnan and  Scott A. Smolka and  Yifei Dong and  Xiaoqun Du and  Abhik Roychoudhury and  V. N. Venkatakrishnan},
title = {{XMC}: A Logic-Programming-Based Verification Toolset},
booktitle = {Twelfth International Conference on Computer Aided Verification ({CAV})},
address = {Chicago, Illinois},
month = {July},
series = {Lecture Notes in Computer Science},
volume = {1855},
publisher = {Springer},
pages = {576--580},
year = {2000}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan