Verification in the Large via Symbolic Approximation

This article describes the technique, symbolic approximation, that we have evolved to handle the post-hoc verification of C code in very large open source projects such as the Linux kernel, essentially consisting of deliberate approximation in a symbolic domain. Using the technique, we are treating millions of lines of C code source in a few hours on very modest support platforms. The theoretical foundation is a configurable compositional programming logic and a notion of approximation that is tied to what can be deduced about a program, in that adjusting the logic for reasoning about it adjusts the goodness of the approximation to it.