From Rules to Analysis Algorithms with Time and Space Guarantees

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

0306399Yanhong A. LiuSUNY @ Stony BrookMany computation problems, including program analysis and model checking problems in particular, are most clearly and easily specified using relational rules. Yet, developing and implementing efficientalgorithms 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 alsoexploit 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 bycomparing automatically generated implementations with other algorithms and implementations. The research results will enable faster and better development and implementations of computer softwarefor solving practical analysis problems. The transformational approach will help assure the correctness and efficiency of the implementations.