Coverity on Wednesday is announcing a software analysis engine based on the concept of "Boolean satisfiability," or SAT.

Featured in the Coverity Prevent SQS (Software Quality System) product, the SAT engine uses a representation of software, or a "software DNA map," to identify complex defects in source code. This helps software development teams eliminate potentially costly defects.

The technology allows Coverity to be more precise and to report a higher percentage of false defects, said Ben Chelf, Coverity's CTO.

"We're the first people to actually take the technology that can solve these types of problems and put it into a static analysis engine for the purpose of finding defects before you already run the program," Chelf said.

The product ensures developers are not bogged down with trying to fix code that is not defective.

The Boolean satisfiability technique, which features patented technology from Coverity, creates a bit-accurate representation of a software system, with software questions translated into Boolean values of true or false and Boolean operators such as "and," "not," and "or." This enables source code to be analyzed by SAT-based Solvers.

The first Solver to be released is the False Pruning Solver, to lower false positive test results in static code analysis. Two more Solvers are planned in early 2008 to check code assertions and detect critical bug categories, including integer overflows. The Solvers also will expand Coverity dataflow analysis capabilities to uncover greater numbers of buffer overflows while maintaining a low false positive rate.

Prevent SQS is available Wednesday for C, C++, and Java software projects. Pricing starts at $35,000 a year for the enterprise-level product.