On 23 April at 13:00, Simmo Saan will defend his doctoral thesis “Correctness Witnesses for Thread-Modular Program Analysis” to obtain the degree of Doctor of Philosophy (in Computer Science).
Supervisor
Assoc. Prof. Vesal Vojdani, University of Tartu
Opponents
Prof. Patrick Cousot, New York University (USA)
Prof. Dirk Beyer, Ludwig-Maximilians-Universität München (Germany)
Summary
Everyone wants software to be fast and to just work (correctly), i.e., not have bugs. Multi-threaded programs can be efficient by executing multiple operations concurrently, but they can be hard to write correctly. Since they are also difficult to test, we must turn to formal verification. This can be automated using static analyzers — other programs which try to verify software automatically. Automated software verifiers are themselves complex programs which may also contain bugs and, thus, produce incorrect results. To make their verdicts more trustworthy, verifiers may produce witnesses that expose their reasoning about the analyzed program. These proof objects allow the analysis results to be inspected by humans or even other programs called witness validators. Unfortunately, before this work there were no verification witnesses for explaining the correctness of multi-threaded programs. Therefore, this thesis aims to fill the research gap by using witnesses to make the analysis of concurrent programs trustworthy, but also performant and precise.
First, the thesis improves the analysis of concurrent programs using abstract interpretation, which is a successful method for verifying real-world software. Second, the thesis studies how abstract interpretation can benefit from witnesses, both in terms of performance and precision. Third, the thesis joins the previous directions and proposes correctness witnesses for concurrent programs, finally filling the research gap. Therefore, this thesis has advanced the state-of-the-art of abstract interpretation and verification witnesses.
Witnesses allow us to develop better static analyzers, which in turn help developers write correct multi-threaded programs.
