The objective of this project is to deploy the latest advances in concurrency research and in logic programming systems to build a software environment called LMC for system specification and verification. LMC's main function is model checking: determining whether a software system possesses a particular formally specified property. LMC is built from two independently developed systems, each of significant interest in its own domain: the Concurrency Factory verification toolkit (developed jointly by Stony Brook and NC State), and the XSB tabled logic programming system (developed by Stony Brook).
![]() |
The LMC project is supported by NSF Grant CCR--9705998. |