Logic Programming and Model Checking

Baoqiu Cui, Yifei Dong, Xiaoqun Du, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Abhik Roychoudhury, Scott A. Smolka, David S. Warren

Abstract:
We report on the current status of the LMC project, which seeks to deploy the latest developments in logic-programming technology to advance the state of the art of system specification and verification. In particular, the XMC model checker for value-passing CCS and the modal mu-calculus is discussed, as well as the XSB tabled logic programming system, on which XMC is based. Additionally, several ongoing efforts aimed at extending the LMC approach beyond traditional finite-state model checking are considered, including compositional model checking, the use of explicit induction techniques to model check parameterized systems, and the model checking of real-time systems. Finally, after a brief conclusion, future research directions are identified.

Bibtex Entry:

@inproceedings{CDD+:PLILP98,
author = {Baoqiu Cui and  Yifei Dong and  Xiaoqun Du and  K. Narayan Kumar and  C. R. Ramakrishnan and  I. V. Ramakrishnan and  Abhik Roychoudhury and  Scott A. Smolka and  David S. Warren},
title = {Logic Programming and Model Checking},
booktitle = {Principles of Declarative Programming},
address = {Pisa, Italy},
month = {September},
series = {Lecture Notes in Computer Science},
volume = {1490},
publisher = {Springer},
pages = {1--20},
year = {1998}
}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)