Shaz Qadeer,
HAVOC: A Precise and Scalable Verifier for Systems Code

HAVOC is a precise and scalable verifier for systems software. HAVOC achieves scalability by performing modular verification. Procedures are annotated with contracts---preconditions, postconditions and modifies clauses---allowing each procedure to be verified separately using the contracts of the called procedures. HAVOC achieves precision by two mechanisms. First, it models the operational semantics of systems code precisely. Second, it supports a specification language that is expressive enough to capture the contracts necessitated by modular verification. The annotation language is based on a core logic, containing universal quantifiers and second-order theories such as arithmetic and reachability, for which the satisfiability problem, despite the expressiveness of the logic, is NP-complete. We have implemented HAVOC on top of the Boogie verification condition generator and the Z3 satisfiability-modulo-theory (SMT) solver. We believe that the advances in SMT solvers and our modular approach will combine well to create a scalable verifier that can be used to verify partial safety specifications of real-world programs. In this lecture, I will present the design and implementation of HAVOC and our experience applying it to check modules in the Windows operating system.