CISE PostDoc: Beyond Finite State Model Checking in LMC

点击翻译按钮获取中文摘要

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.