CISE PostDoc: Beyond Finite State Model Checking in LMC

Ramakrishnan，C. R. 作者声明：A. Warren，大卫，S. 纽约州立大学斯托尼布鲁克分校 CISE PostDoc：超越LMC中的有限状态模型检查 模型检测是验证并发系统性质的一种重要新兴技术。 基于逻辑的模型检查（Logic-Based Model Checking，LMC）项目的主要目标是基于并发研究和表逻辑编程的最新进展来构建简洁高效的模型检查器。最初的结果包括一个模型检查器的值传递CCS（指定并发系统的语言）和模态μ演算（一种表达的时态逻辑），写在不到200行的表Prolog代码，与其他当代系统的性能相当。 到目前为止，LMC项目一直专注于有限状态系统的模型检查。 目前项目支持的博士后候选人将通过使用约束表格逻辑编程的功能和多功能性来验证无限状态系统，从而扩大LMC项目的范围。 例如，通过约束来表示状态集合允许使用基于案例的推理来验证某些无限状态系统。 此外，使用约束和表格进行编程有助于将演绎策略（如归纳法）与算法模型检查更紧密地结合起来。由此产生的技术将允许验证无限系列的系统（例如，对于任何N，具有N个参与者的协议），而不必单独验证每个实例。

9805735 Ramakrishnan, C. R. Ramakrishnan, I.V. Smolka, Scott, A. Warren, David, S. SUNY at Stony Brook CISE PostDoc: Beyond Finite State Model Checking in LMC Model checking is a key emerging technique for verifying properties of concurrent systems. The primary objective of the LMC (Logic-Based Model Checking) project is to build succinct and efficient model checkers based on the latest advances in concurrency research and tabled logic programming. Initial results include a model checker for value-passing CCS (a language for specifying concurrent systems) and the modal mu-calculus (an expressive temporal logic), written in less than 200 lines of tabled Prolog code, with performance comparable to that of other contemporary systems. The LMC project has, until now, focused on model checking finite-state systems. The Postdoctoral Candidate supported by the current project will expand the scope of the LMC project by using the power and versatility of constraint tabled logic programming to verify infinite-state systems. For instance, representing sets of states by constraints permits use of case-based reasoning for finitely verifying certain infinite-state systems. Moreover, programming with constraints and tables facilitates tighter integration of deductive strategies, such as induction, with algorithmic model checking. The resulting technology will permit verification of an infinite family of systems (e.g. a protocol with N participants, for any N), without having to verify each instance separately.