SLAM2: Static driver verification with under 4% false alarms

In theory, counterexample-guided abstraction refinement (CEGAR) uses spurious counterexamples to refine overapproximations so as to eliminate provably false alarms. In practice, CEGAR can report false alarms because: (1) the underlying problem CEGAR is trying to solve is undecidable; (2) approximations introduced for optimization purposes may cause CEGAR to be unable to eliminate a false alarm; (3) CEGAR has no termination guarantee - if it runs out of time or memory then the last counterexample generated is provably a false alarm. We report on advances in the SLAM analysis engine, which implements CEGAR for C programs using predicate abstraction, that greatly reduce the false alarm rate. SLAM is used by the Static Driver Verifier (SDV) tool. Compared to the first version of SLAM (SLAM1, shipped in SDV 1.6), the improved version (SLAM2, shipped in SDV 2.0) reduces the percentage of false alarms from 25.7% to under 4% for the WDM class of device drivers. For the KMDF class of device drivers, SLAM2 has under 0.05% false alarms. The variety and the volume of our experiments of SDV with SLAM2, significantly exceed those performed for other CEGAR-based model checkers. These results made it possible for SDV 2.0 to be applied as an automatic and required quality gate for Windows 7 device drivers.