Coverity, Inc. today announced Prevent SQS, the first software analysis engine based on Boolean satisfiability (SAT). Leveraging a representation of software, or Software DNA Map, Coverity's SAT engine is designed to automatically identify complex defects in source code with unmatched precision and accuracy.
Unlike current static analysis engines that rely on dataflow analysis and multiple check-ers to identify software defects, the SAT engine is based on Boolean satisfiability and will enable multiple SAT solvers to identify software defects. This new technique of source code analysis is made possible by patent-pending technology from Coverity that creates a bit-accurate representation of a software system, where each possible soft-ware operation is translated into Boolean values (true and false) and Boolean operators (such as and, not, or). This bit-accurate representation enables source code to be ana-lyzed by SAT-based Solvers for the first time in commercial computer programming.
Available today, Coverity's False Path Pruning SAT Solver is the first Solver to be re-leased for Prevent SQS. The False Path Pruning Solver significantly lowers the number of false positive results in static code analysis. By leveraging SAT to determine if the path to a potential software defect is feasible, the solver identifies and excludes unfea-sible defects. By 'pruning' these unfeasible results, the Solver increases the overall ac-curacy of code analysis results and allows developers to focus on defects that pose a genuine threat to the success of their projects.
Coverity Prevent SQS checks one hundred percent of the paths in C, C++ and Java software pro-jects. It also analyzes software dependencies, key third-party libraries, and projects spread across multiple development groups. Coverity Prevent SQS is available immediately, and is priced based on project size. For more information, visit www.coverity.com.