Synthesis is the process of computing an implementation from a specification of the desired behavior, performance, and security and privacy properties. This ideal form of system design has been a long-standing dream in computer science. The goal of this project is to realize the dream of synthesis, in the same way that current tools for program analysis and model checking realize the dream of verifying program correctness. This is feasible today due to the enormous computing power of today's platforms and due to the recent significant technical advances in the underlying technologies for program analysis and verification. Synthesis, supported by powerful computational tools, and integrated into system design, can have a transformative effect by enabling the construction of more complex and more robust systems than are currently possible or cost effective. The focus of this project is the development of algorithmic tools for assertion-based design synthesis. We will develop automata- and game-theoretic approach to assertion-based intentional system design. The intellectual merit of this project is the interplay between games, automata, and logic. Based on deep theoretical foundations, prototype synthesis tools will be developed. These are crucial for the development of reliable, secure, and scalable computing systems.
Eager: Automated Synthesis for System Design