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.