From Rules to Analysis Algorithms with Time and Space Gaurantees

Many computation problems, including program analysis and model checking problems in particular, are most clearly and easily specified using realtional rules. Yet, developing and implementing efficient algorithms for these problems is a nontrivial, recurring task. This project proposes to develop a unified method for transformaing rule-based specifications and transformations to provide both time and space guarantees for the derived algorithms. We will focus in particular on rule-based specifications for program analysis and model checking problems and develop fully automatic methods for the transforamtions and the time and space analysis in this domain.