CISE PostDoc: Beyond Finite State Model Checking in LMC

CISE 博士后：LMC 中超越有限状态模型检查

• 批准号: 9805735
• 负责人: Coimbatore Ramakrishnan
• 金额: $ 6.6万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-09-01 至 2001-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9805735&HistoricalAwards=false
• 关键词: CISE; PostDoc; Beyond; Finite; State

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.

9805735 Ramakrishnan，C.R.Ramakrishnan，I.V.Smolka，Scott，A.Warren，David，S.SUNY，Stony Brook cise博士后：超越有限状态模型检测是验证并发系统性质的一种关键新兴技术。LMC(基于逻辑的模型检查)项目的主要目标是基于并发研究和表式逻辑编程的最新进展来构建简洁高效的模型检查器。初步结果包括用于传递值的CCS(一种用于指定并发系统的语言)的模型检查器和用不到200行表格PROLOG代码编写的模式u演算(一种富有表现力的时态逻辑)，其性能可与其他当代系统相媲美。到目前为止，LMC项目一直专注于有限状态系统的模型检查。当前项目支持的博士后候选人将利用约束表逻辑编程的能力和通用性来验证无限状态系统，从而扩大LMC项目的范围。例如，用约束表示状态集允许使用基于案例的推理来有限地验证某些无限状态系统。此外，使用约束和表进行编程有助于将演绎策略(如归纳)与算法模型检查更紧密地结合在一起。由此产生的技术将允许验证无限的系统家族(例如，对于任何N个参与者，具有N个参与者的协议)，而不必单独验证每个实例。