Logic Programming and Model Checking
C.R. Ramakrishnan
Scott Smolka
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.
The slides used in the talk are available in
Postscript(gzipped) and
PDF.
The material used in the talk are described in a
companion paper
"Logic Programming and Model Checking"
that appeared in PLILP/ALP'98 proceedings
(published by Springer).