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.