As computerized systems are becoming larger, more complex, and increasingly distributed, a larger and larger portion of the design effort goes into the validation and verification effort. There is a growing need for formal methods that guarantee systems reliability, correctness, and efficiency by design. The investigators will address this challenge by contributing to the the establishment of a theory of automated design synthesis of computing systems. The new techniques will enable the development of systems of higher quality within shorter design cycles and with lower costs. The goal of the project is the development of a fundamental theory for automated system design synthesis. The ultimate goal is a demonstrable improvement in design productivity.
The focus of this project will be the development of algorithmic tools for assertion-based design synthesis. The investigators will develop automata- and game-theoretic approach to assertion-based intentional system design. While the main focus of games and automata has traditionally been on finite objects (or very simple infinite ones), it is necessary to extend this approach to the more complex situations that we face in most practical applications, and for which the method is not yet adequately developed or exploited. The intellectual merit of this project is the interplay between games, automata, and logic. Our aim is to make fundamental progress in this area, aimed at the development of automated design techniques. These are crucial for the development of reliable, robust, and scalable computing systems.
