< Back to previous page


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).

Date:21 Jun 2016 →  21 Jun 2020
Keywords:program verification
Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences
Project type:PhD project