CAREER: Tabled Logic Programming for Verification and Program Analysis

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

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.