Eager: Automated Synthesis for System Design

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

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.