Modular Verification of Shared-Memory Concurrent Systems Software

In this talk, I will give an overview of the main software verification research in my group right now, by my student Zvonimir Rakamaric.

Zvonimir has decided to target particularly high-value software: the low-level systems software that everything else depends on, e.g., device drivers, operating systems, virtual machine monitors, hypervisors, etc. In this domain, the soundness of the verification approach is important, and the only sound verification technique that has demonstrated sufficient scalability and precision is a modular approach (with manual annotations of pre-conditions, post-conditions, loop invariants, etc.). Unfortunately, a modular approach has many problems dealing with systems software, and our research has been a step-by-step attack on these problems. Results so far are: reducing the effort of annotation by automating the generation of most frame axioms; developing a flexible memory model that accurately handles type-unsafe, low-level code, yet is still scalable; and an approach to analyze (bounded context swap) low-level, concurrent software.

Zvonimir's tools have discovered several real bugs in real software, and he is currently doing an internship at Microsoft Research with the goal of further, practical applications of his tools.