Abstract

he application of software-verification technology towards building
realistic bug-finding tools requires working through several
precision-scalability tradeoffs. For instance, a critical aspect while
dealing with C programs is to formally define the treatment of
pointers and the heap (usually termed as the “memory
model”). A machine-level modeling is often intractable, whereas one
that leverages high-level information (such as types) can be
inaccurate. Another tradeoff is modeling integer arithmetic. Ideally,
all arithmetic should be performed over bitvector representations
(like what happens in the hardware), whereas the current practice in
most tools is to use mathematical integers for scalability. A third
tradeoff, in the context of bounded program exploration, is to choose
a bound that ensures enough coverage without overwhelming the
analysis.

This paper works through these three tradeoffs when we applied Corral,
an SMT-based verifier, inside Microsoft’s Static Driver Verifier
(SDV). Our decisions were guided by experimentation on a large set of
drivers; the total verification time exceeded well over a month. We
justify that each of our decisions were crucial in getting value out
of Corral and led to Corral being accepted as the engine that powers
SDV in the Windows 8.1 release, replacing the SLAM engine that had
been used inside SDV for the past decade.

This paper won the Distinguished Paper Award at FSE 2014.