Logic Programming and Model Checking

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 speci cation and veri cation. 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 e orts aimed at extending the LMC approach beyond traditional nite-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 identi ed.

• Type: Conference
• Year: 1998
• Where: PLILP
• Authors: Baoqiu Cui, Yifei Dong, Xiaoqun Du, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Abhik Roychoudhury, Scott A. Smolka, David Scott Warren
• Keywords: Automated Reasoning, Model Checking, Nite-state Model Checking, PLILP 1998, XMC Model Checker