I'm proud to announce Coverity has been issued a new patent Methods for Selectively Pruning False Paths in Graphs That Use High-Precision State Information. The patent covers techniques that apply modern solvers such as SAT and SMT to the problem of eliminating false paths in programs. False paths are one of the main causes of false positives in static analysis results - in our measurements of open source software, the techniques in this patent eliminates 1/3 of all false positives.
The naive way of leveraging solvers in false path pruning analyzes only one path at a time, or converts a whole function at a time into a constraint problem. Both of these approaches fail on larger code bases. Real-world programs have an exponentially large number of paths, even within single functions. And converting entire functions doesn't scale when interprocedural analysis is needed. Worse, these methods don't play well with existing analysis infrastructure that is closer to dataflow analysis. The techniques in this patent address these concerns by generalizing from proofs provided by SAT/SMT solvers that certain paths are infeasible. The proofs isolate the core contradictions that occur between path conditions, which can then be quickly tested for on other paths. This can rule out an exponentially large number of infeasible paths without invoking the solver on large numbers of redundant constraint sets.
This technology has been in Coverity's product for a few years now. All modern versions of Coverity Quality Advisor include this technology under the --enable-constraint-fpp option. It's all part of our ongoing efforts to continually improve our analysis results using the latest technologies.