Modular Formal Verification of Total Correctness Properties of Concurrent Imperative Programs

For software development projects with very high correctness requirements (including safety requirements, security requirements, responsiveness requirements, or real-time requirements), in many cases insufficient assurance of correctness can be obtained through classical quality assurance techniques such as testing and code review. In contrast, the alternative approach of formal verification, where mathematical methods are used to mathematically formalize and prove that the system meets the intended correctness properties, can offer much higher assurance. In this project, I will perform research on improving the state of the art in this area to make it more economically feasible to apply formal verification in practice and enable software development teams to deliver high-assurance products cost-effectively. I will focus in particular on the important but complex aspects of total correctness (as opposed to partial correctness, where issues of termination and liveness are ignored) and concurrency (where the program specifies only a partial order on the execution steps, leading to an explosion of possible executions).