Practical Verification of Distributed Systems: Streamlining Safety Proofs Using Invariant Taxonomies, and Verifying Latency Properties Using Symbolic Latency

Abstract

Formal verification promises software that is much more robust, and even bug-free, compared to the traditional approach of testing. However, its widespread adoption is hindered by limitations in its practicality. This dissertation addresses two major barriers to applying formal verification to distributed systems software, namely its ease of use and its application to broader non-functional properties. In particular, it demonstrates that verification of functional safety properties can be made significantly easier in the general undecidable setting by leveraging the concept of an invariant taxonomy, and that verification can be extended to non functional safety properties, such as reasoning about the end-to-end latency of distributed systems.