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

Abstract:
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:

@inproceedings{RRS+:CAV00,
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
(cram@cs.sunysb.edu)