Mechanized verification of liveness properties of concurrent, imperative programs

Many tools and techniques exist for formal verification of imperative programs. However, for most of them, there is significant room for human error, both in applying the tools and in building the tools. This reduces the reliability of the results. Mechanized verification aims to address this issue by reducing the trusted computing base of a verification technique to a small kernel. It is well-vetted, has explicit and clearly defined machine-readable semantics of the target platform and a relatively small, trusted checker of proofs expressed in a generic higher-order logic, usually based on the lambda calculus. Current state-of-the-art frameworks such as Iris for the machine-checked verification of concurrent imperative programs do not support the verification of liveness properties of concurrent programs, such as the property that a server will always eventually respond to each request. We will build upon recent advances in pen-and-paper logics for such verification to extend the popular Iris framework with support for liveness verification.