Multi-threaded programs can be efficient by executing multiple operations concurrently, but they can be hard to write correctly. They are also difficult to test because thread scheduling is non-deterministic. Thus, formal verification is vital for developing multi-threaded software. 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, there were previously 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.
Our solution relies on abstract interpretation, which is a successful method for verifying real-world software and multi-threaded programs. First, this thesis investigates the value analysis of concurrent programs using abstract interpretation. We find existing approaches to be incomparable and devise new thread-modular analyses, which are more precise than prior work. Second, this thesis studies how abstract interpretation can benefit from witnesses, both in terms of performance and precision. We achieve both benefits by introducing a novel unassume operation, and use it to develop the first witness validator using abstract interpretation. Third, this thesis joins the previous directions and proposes correctness witnesses for concurrent programs, thereby filling the research gap. We propose two different flavors of witnesses, which respectively correspond to a local and a global view of concurrency, and experimentally evaluate them.
All of the ideas are implemented in the Goblint static analysis framework, which is based on abstract interpretation. Thus, this thesis also provides an up-to-date overview of the framework and its progress. Our work with witnesses has revealed pre-existing bugs in Goblint and their fixes have improved it overall. Therefore, this thesis advances 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.