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.