Project Overview

The LMC (Logic Programming-Based Model Checking) project deploys the latest advances in concurrency research and in logic programming systems to build a software environment for system specification and verification. The project is focussed on model checking--- determining whether a system specification possesses a property expressed as a temporal logic formula--- but the techniques we propose are applicable to any verification methodology requiring fixed-point computation (e.g., bisimulation and refinement checking).

The LMC environment builds on two existing software systems that have helped advance the state of the art in their respective fields---the Concurrency Factory specification and verification environment, and the XSB tabled logic programming system. Both of these systems have been developed at the Stony Brook Department of Computer Science, and this project brings together for the two groups of researchers responsible for these systems. The anticipated benefits from a logic programming-based approach to model checking include the following:

The directions of current research in the LMC project are: Work is also underway in enhancing the XSB tabled logic programming system with the LMC project as the primary application:
Last modified: Thu Jul 2 16:52:39 EDT 1998