LMC: A System for the Specification and Evaluation of Logic-Based Model Checking

这个项目的目标是利用并发研究和逻辑编程系统的最新进展来建立一个称为LMC的软件环境，用于系统规范和验证。LMC的主要功能是模型检查：确定软件系统是否具有特定的正式指定属性。LMC由两个独立开发的系统构建，每个系统在其自己的领域都非常重要：并发工厂验证工具包(由Stony Brook和NC State联合开发)和XSB表逻辑编程系统(由Stony Brook开发)。这项研究的预期好处包括：XSB中的模型检查器是在语义等式级别指定的，这意味着特定规范语言和逻辑的系统可以用数百行XSB代码而不是数万行C代码编写；XSB的可编程性允许直接编码重要的模型检查优化；在XSB中，可以将任意的模型检查计算步骤与演绎步骤交织在一起，而不会影响前者的性能。这些功能有望使LMC成为正式确保关键软件系统(如网络协议)正确性的实用工具。

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 anticipated benefits of this research include the following: a model checker in XSB is specified at the level of semantic equations, meaning a system for a specific specification language and logic can be coded in several hundred lines of XSB code rather than in tens of thousands of lines of C++ code; the programmability of XSB allows for direct encoding of important model checking optimizations; in XSB it is possible to interleave arbitrarily model checking computational steps with deduction steps without penalizing the performance of the former. These features are expected to make LMC a practical tool for formally assuring the correctness of critical software systems such as network protocols.