Program Verification and Synthesis for Reliable Concurrent and Distributed Computing

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.

由于计算机在我们生活的各个方面的不断增强，确保软件的可靠性一直是一个迅速增长的关注点。在关键系统上执行的软件可靠性的重要性，例如医疗设备，飞行控制系统，核电站，自动驾驶汽车，金融引擎和移动设备，这不能被夸大，这证明了软件故障产生了数十亿美元成本甚至损害人类现场的实例。软件可靠性的计算机辅助保证属于两个主要的互补学科：验证和综合。程序验证是编程语言和软件工程的子学科，旨在构建自动化工具，以确保以前编写的程序的正确性。程序合成试图根据高级规格自动生成正确可靠的构造代码，从而首先消除了继承的人为错误（和成本）。由于单个基于硅的处理器的性能增长速度降低，重点一直在转向同时利用多个处理器的程序，或者对内存层次结构，处理周期，电源管理和硬件的其他方面的明智优势，以取得更好的整体性能。考虑到这些额外的约束，使编程过程变得非常复杂，并大大提高了确保可靠性的复杂性。众所周知，对于多核心处理器或分布式环境（云）的编程很容易出错，这是由于无确定性和难以预测的代码组件之间同时执行不同处理器执行的组件之间的交互。其他现代软件平台还带有现代可靠性问题，例如安全性和隐私保证。分布式计算中的另一个新兴领域是自主或半自主的代理，它们与环境或彼此相互作用以执行某些任务。物联网（IOE）和机器人系统是此类系统的两个众所周知的例子。如何自动为单个代理商或协调员开发可靠的控制器的问题的问题大多是出乎意料的。拟议的研究将旨在通过设计属于计划验证和综合类别的新技术和工具的设计，以在近似领域的软件可靠性中提高最新技术。我们提出的研究在这些领域寻求理论和技术进步。理论发展将以逻辑，自动机理论和算法的新结果的形式形式，而技术进步将由可自动验证现有代码可靠性的新工具和技术组成，或自动合成此类系统的可靠软件。