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. |
Contact: lmc@cs.sunysb.edu
Last modified: Mon Jan 11 12:25:13 EST 1999