Program Verification and Synthesis for Reliable Concurrent and Distributed Computing

由于计算机在我们生活的方方面面扮演着越来越重要的角色，确保软件的可靠性已经成为一个迅速增长的问题。在医疗设备、飞行控制系统、核电站、自动驾驶汽车、金融引擎和移动设备等关键系统上执行的软件可靠性的重要性再怎么强调也不为过，因为大量的软件故障已经造成了数十亿美元的损失，甚至伤害了人类的生命。计算机辅助软件可靠性保证属于两个主要的互补学科：验证和综合。程序验证是编程语言和软件工程的一个分支学科，旨在构建自动化工具来确保先前编写的程序的正确性。相反，程序合成试图根据高级规范自动生成可证明可靠的代码，从而首先消除固有的人为错误（和成本）。由于单个硅基处理器的性能增长率放缓，重点已经转向同时利用多个处理器的程序，或者利用内存层次结构、处理周期、电源管理和硬件的其他方面来获得更好的整体性能。考虑到这些额外的约束会使编程过程变得非常复杂，并且大大增加了确保可靠性的复杂性。众所周知，多核处理器或分布式环境（云）的编程容易出错，因为在不同处理器上同时执行的代码组件之间存在不确定性和难以预测的交互。此外，现代软件平台带来了现代可靠性问题，例如安全和隐私保证。分布式计算中的另一个新兴领域是自主或半自主代理，它们与环境或彼此交互以执行某些任务。物联网（IoE）和机器人系统是这类系统的两个众所周知的例子。如何为单个代理自动开发或认证可靠的控制器或为一组代理自动开发或认证可靠的协调器的问题大多未被探索。拟议的研究将旨在通过设计属于程序验证和综合两类的新技术和工具，在上述领域推进软件可靠性的最新技术。我们提出的研究在这些领域寻求理论和技术上的进步。理论的发展将以逻辑、自动机理论和算法的新结果的形式出现，而技术的进步将包括新的工具和技术，可用于自动验证现有代码的可靠性，或自动为此类系统合成可靠的软件。

Due to ever-increasing role of computers in about every aspect of our lives, ensuring reliability of software has been a rapidly growing concern. The importance of reliability of software executed on crucial systems such as medical devices, flight control systems, nuclear stations, self-driving cars, financial engines, and mobile devices cannot be exaggerated as evidenced by the abundance of instances where software failure has incurred billions of dollars in costs and even harmed human lives. Computer-aided assurance of software reliability falls under two major complementary disciplines: Verification and Synthesis. A sub-discipline of both programming languages and software engineering, program verification aims at building automated tools for ensuring correctness of previously written programs. Program synthesis attempts instead to automatically generate code that is provably reliable by construction, based on high level specifications, thereby eliminating the inherent human error (and cost) in the first place. As a result of the slow-down in the performance growth rate of individual silicon-based processors, emphasis has been shifting towards programs that exploit multiple processors at the same time or take informed advantage of memory hierarchies, processing cycles, power management and other aspects of hardware for better overall performance. Taking these additional constraints into account hugely complicates the programming process and dramatically increases the complexity of ensuring reliability. Programming for multicore processors or distributed environments (the cloud) are notoriously error prone due to nondeterministic and hard-to-predict interactions between components of code that execute simultaneously on different processors.  Additionally, modern software platforms come with modern reliability concerns such as security and privacy assurances. Another emerging area in distributed computing is that of autonomous or semi-autonomous agents which interact with their environments or each other to perform certain tasks. Internet of Things (IoE) and robotic systems are two well-known examples of such systems. The problems of how to automatically develop or certify reliable controllers for individual agents or coordinators for a collection of agents are mostly unexplored.  The proposed research will aim at advancing the state of the art in software reliability in the aforementioned areas through the design of new techniques and tools that fall under both categories of program verification and synthesis. Our proposed research seeks both theoretical and technological advancements in these areas.  The theoretical developments will be in the form of new results in logic, automata theory, and algorithms, while technological advances will consist of new tools and techniques that can be used to automatically verify the reliability of existing code, or automatically synthesize reliable software for such systems.