Increasing The Practicality Of Verification Using Incomplete Solutions

Hybrid Event:  Zoom / 3941 BBB

Abstract: Building correct and robust software systems is challenging. To ensure correctness, developers have increasingly turned to formal verification to help achieve this goal. Verification is attractive because it provides strong assurances of correctness by construction. However, two fundamental challenges limit these 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 Satisfiability Modulo Theories (SMT) solvers. These shortcomings inevitably require manual effort and expertise to overcome, deterring the broader adoption of automated verification.

This dissertation demonstrates how heuristic-based techniques can assist developers in overcoming the fundamental limitations of verifying programs with automated theorem provers. First, it explores how classical 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. A proof may fail for various 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 identify hints about why a proof failed by creating and verifying a finite approximation of the original program.

Finally, in the pursuit of building robust software systems, this dissertation extends our theoretical understanding of the Paxos protocol. 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.