Static Assertion Checking of Production Software with Angelic Verification

The ability to statically detect violations of assertions can add great value to developers.
However, in spite of decades of progress in program verification, static assertion checking is far from being cost-effective for production software.
The two main obstacles to finding high-quality defects are (a) false alarms due to under-constrained environment, and (b) finding violations to deeply nested procedures.

In this talk, we will describe our experience with the angelic verification (AV) tool for statically finding assertion violations in real-world software. The basic idea of AV is to pair an interprocedural assertion verifier with a framework for automatic inference of likely specifications on unknown values from the environment. We will summarize the approach, and will focus on design choices required to find high-quality violations of memory-safety with low false alarms. We discuss some results on Microsoft codebases and open source software, and challenges ahead.