Eager: Automated Synthesis for System Design

综合是从所需行为、性能、安全性和隐私属性的规范计算实现的过程。 这种理想的系统设计形式一直是计算机科学中的一个长期梦想。 这个项目的目标是实现综合的梦想，就像当前的程序分析和模型检查工具实现验证程序正确性的梦想一样。这在今天是可行的，这是由于当今平台的巨大计算能力以及由于用于程序分析和验证的底层技术的最近重大技术进步。综合，由强大的计算工具支持，并集成到系统设计中，可以通过使更复杂和更强大的系统比目前可能的或成本efficient.The项目的重点是基于断言的设计综合算法工具的开发建设具有变革性的影响。 我们将发展自动机和博弈论的方法，以断言为基础的有意系统设计。 这个项目的智力价值是游戏，自动机和逻辑之间的相互作用。 基于深厚的理论基础，原型合成工具将被开发。 这些对于开发可靠、安全和可扩展的计算系统至关重要。

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.