CAREER: Tabled Logic Programming for Verification and Program Analysis

9876242 Ramakrishnan， C. R.逻辑程序的表格解析解决了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.