CAREER: Tabled Logic Programming for Verification and Program Analysis

职业：用于验证和程序分析的表格逻辑编程

• 批准号: 9876242
• 负责人: Coimbatore Ramakrishnan
• 金额: $ 20.34万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-08-01 至 2004-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9876242&HistoricalAwards=false
• 关键词: CAREER; Tabled; Logic; Programming; Verification

9876242 Ramakrishnan, C. R. Tabled resolution for logic programs addresses the major shortcomings of Prolog-style resolution, namely, weak termination, repeated subcomputations, and weak semantics for negation. Tabled logic programming enables development of many applications at a high level without sacrificing efficiency. For instance, techniques used for program analysis and verification, such as model checking and abstract interpretation, can be implemented using tabling by treating the semantic equations as logic rules. This project focusses on (i) exploiting the power of current tabled resolution systems to construct high-performance program analyzers and model checkers for systems specified in various process languages and properties specified using different temporal logics; (ii) extending tabling methods to constraint logic programs, thereby tackling new applications, such as verification of infinite-state and real-time systems; and (iii) integrating deductive strategies (traditionally used by theorem provers) into model checkers by combining tabled resolution with program transformation techniques. This combination offers novel solutions to problems such as verification of parameterized systems, analysis of security vulnerabilities of computer systems, and scheduling in workflow systems. The project plans to incorporate research results into the classroom by adding a two-week unit on program analysis to a Compiler Design course, and developing new courses on computer security and program transformations.

9876242 拉马克里希南角R.逻辑程序的表格解析解决了Prolog风格解析的主要缺点，即弱终止，重复的子计算和弱否定语义。 表格逻辑编程使得在不牺牲效率的情况下在高水平上开发许多应用成为可能。 例如，用于程序分析和验证的技术，如模型检查和抽象解释，可以通过将语义方程视为逻辑规则来使用制表来实现。该项目的重点是（i）利用当前表格解析系统的能力，为各种过程语言指定的系统和使用不同时态逻辑指定的属性构建高性能的程序分析器和模型检查器;（ii）将表格方法扩展到约束逻辑程序，从而解决新的应用，例如无限状态和实时系统的验证;以及（iii）通过将表格解析与程序转换技术相结合，将演绎策略（传统上由定理证明器使用）集成到模型检查器中。 这种组合提供了新的解决方案，如验证参数化系统，计算机系统的安全漏洞分析，工作流系统中的调度问题。 该项目计划将研究成果纳入课堂，在计算机设计课程中增加为期两周的程序分析单元，并开发有关计算机安全和程序转换的新课程。