SHF: Small: Tool Support for Verifiably-Robust Software

点击翻译按钮获取中文摘要

Society increasingly relies on software in critical roles for which crashes can have serious consequences including the loss of lives. For example, it is now commonplace for software to control the engines and brakes in our cars. This research investigates a new approach for improving the resilience of software. The goal is to verify that hidden bugs cannot cause programs to transition into problematic states in which they stop responding to human control or respond differently than when they were tested. Given the scale that our society depends on software in critical roles, new approaches to improving software resilience have the potential to reduce the financial costs of software failures and even save lives.Previous work on software resilience largely focused on extensive testing or formal verification of correctness. This project takes a new approach - it seeks to verify that the consequences of a software error have a limited scope in time. Precisely, it verifies that after a bounded time period after an error, the execution will reach a state in which it will respond with same behaviors seen while testing. This property is known in the distributed systems literature as self-stabilization. The project will combine type annotations with compiler analyses to verify that a computation is self-stabilizing. A second thrust of the project is to explore how to compose self-stabilizing computations with stateful computations while still providing useful system level guarantees.