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.