From Rules to Analysis Algorithms with Time and Space Guarantees

0306399 Yanhong A. Liu SUNY @ Stony Brook Many computation problems, including program analysis and model checking problems in particular, are most clearly and easily specified using relational rules. Yet, developing and implementing efficient algorithms for these problems is a nontrivial, recurring task. This project proposes to develop a unified method for transforming rule-based specifications into efficient algorithms and characterize the specifications and the transformations to provide time and space guarantees for the derived algorithms. The project will focus on rule-based specifications for program analysis and model checking problems and develop fully automatic methods for the transformations and the time and space analysis in this domain. The development will use a general transformational method that makes computation proceed in an iterative and incremental fashion, analogous to integration by differentiation in calculus. The method will also exploit sophisticated structures for storing and accessing complex data. The project also proposes to implement these methods, apply them to existing and new analysis problems, and evaluate them by comparing automatically generated implementations with other algorithms and implementations. The research results will enable faster and better development and implementations of computer software for solving practical analysis problems. The transformational approach will help assure the correctness and efficiency of the implementations.