Ben Chelf and Andy Chou
Coverity

Static source code analysis has long had a mixed reputation among development teams, due to long analysis times, excessive noise, or an unacceptable rate of false-positive results. Despite these early shortcomings, however, the promise of static analysis has remained of interest to developers because of its ability to find bugs before software is run, improving code quality and dramatically accelerating the availability of new applications.

Now, a groundbreaking new use of Boolean satisfiability (SAT) in the field is poised to help static analysis deliver on its potential. This paper provides a brief overview of static analysis and explains how the use of SAT can enable developers to improve the quality and security of their code by identifying a greater number of critical defects, with the lowest rate of false-positive results in the industry.