CAREER: Tabled Logic Programming for Verification and Program Analysis

9876242逻辑程序的表式归结解决了PROLOG式归结的主要缺点，即弱终止性、重复子计算和对否定的弱语义。表逻辑编程允许在不牺牲效率的情况下在高水平上开发许多应用程序。例如，用于程序分析和验证的技术，如模型检查和抽象解释，可以通过将语义等式视为逻辑规则而使用表来实现。该项目致力于(I)利用现有的表式归结系统的能力，为以各种过程语言和使用不同时态逻辑指定的性质指定的系统构建高性能的程序分析器和模型检查器；(Ii)将表式方法扩展到约束逻辑程序，从而处理新的应用，例如无限状态和实时系统的验证；以及(Iii)通过将表式归结和程序转换技术相结合，将演绎策略(传统上由定理证明者使用)集成到模型检查器中。这种组合为验证参数化系统、分析计算机系统的安全漏洞以及工作流系统中的调度等问题提供了新颖的解决方案。该项目计划将研究成果纳入课堂，在编译器设计课程中增加一个为期两周的程序分析单元，并开发关于计算机安全和程序转换的新课程。

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.