Increasing The Practicality Of Verification Using Incomplete Solutions

Abstract

Building correct software systems is challenging. To ensure correctness, developers have increasingly turned to formal verification to help achieve this goal. Verification provides strong assurances of correctness by construction. Developers write proof annotations to show that their implementation adheres to desired properties captured in a formal specification. Checking if the implementation meets the specification is automated by encoding the proof, specification, and implementation as a satisfiability query and is checked by a Satisfiability Modulo Theories (SMT) solver. However, two fundamental challenges limit the guarantees and the ease of verifying programs with automated theorem provers: the inability to prove the correctness of a specification and the incompleteness of underlying SMT solvers. These shortcomings inevitably require manual effort and expertise to overcome, deterring the broader adoption of automated verification.

This dissertation demonstrates how lightweight techniques can assist developers in overcoming the fundamental limitations of verifying programs with automated theorem provers. First, it explores how classic testing practices can be adapted to test formal specifications. Accordingly, this dissertation presents IronSpec, a specification testing framework that integrates automatic and manual testing techniques to enhance the reliability of formal specifications. Next, this dissertation examines the debugging challenges of failing proofs. Even with a correct specification, a proof may fail for different reasons; unfortunately, underlying SMT solvers do not differentiate between them. To help resolve these debugging dilemmas, this dissertation introduces the Finitized Proof Projection technique and a proof assistant, ProofLens. ProofLens embodies this technique, helping to identify hints about why a proof failed by creating and verifying a finite approximation of the original program.

Finally, as an application of formal verification and in the greater pursuit of building robust systems, this dissertation proves that the original criteria for learning values in the Paxos protocol is stronger than necessary. While verification helps ensure program correctness, it cannot guard against hardware failures. Paxos is a standard building block in state machine replication, a practice commonly used to build robust systems in the presence of hardware failures. This dissertation proves how the discrete numbering of ballots in Paxos enables a safe relaxation of the criteria for learning values.