Deductive Verification for Systems Software
Date: Thu, June 06, 2019
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.
Klaus von Gleissenthall (University of California) | Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Next: Guido Salvaneschi | Language Abstractions for Distributed Software Systems