Deductive Verification for Systems Software

Alex Summers


Date: Thu, June 06, 2019
Time: 09:00
Room: 0.E220 Social Data Lab


Software is used in every corner of our society, and deployed at ever-increasing scale and complexity. The challenges of producing reliable software are compounded by a wide variety of commonplace programming concerns, including mutable shared state, dynamic memory management, (fine-grained) concurrency, asynchronous and distributed communication and weak memory architectures. Formal verification research offers rich techniques for reasoning in these complex settings, but their application is often difficult in practice, both due to conceptual overhead and the substantial effort required in constructing a correct proof.

In this talk, I will outline several of my own research directions, which collectively aim to enable deductive verifiers: tools which, given appropriate specifications of a program’s intended behaviour, can check whether a correctness proof exists. This goal requires a combination of methodological work (on proof techniques, and how to specify a programmer’s intentions) and tool-oriented research on encoding program correctness problems using intermediate verification languages and, ultimately, SMT solvers.

As an example of my projects within this space, I will introduce Prusti, in which we are building verification tools for the Rust language. In particular, we aim in this work to exploit information from Rust’s own type system to enable specification and verification at level of abstraction matching the programming language itself.

Previous: Klaus von Gleissenthall (University of California) |
Next: Guido Salvaneschi |