Next Gen Static Analysis of Code

I came across this white paper illustrating the next generation static analysis of code using boolean satisfiability (SAT). This is an interesting read. It tells you how to use SAT in static analysis to improve code quality and security by identifying a greater number of critical defects in the code with lowest rate of false-positive results.

The white paper can be found here.