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.