Coverity Announces Breakthrough Software Code Analysis Engine

September 19, 2007: Coverity announced at Embedded Systems Conference (ESC) in Boston the first software analysis engine based on Boolean satisfiability (SAT).
Coverity’s SAT engine leverages a highly accurate representation of software, or Software DNA Map, to automatically identify complex defects in source code with unmatched precision and accuracy. By helping software development teams find and eliminate these potentially costly defects, Coverity Prevent accelerate the ability of companies to deliver secure, high quality applications.
"Software developers today need static analysis to become more powerful, predictable and accurate to facilitate the acceleration of the overall software development cycle," said Theresa Lanowitz, founder of voke, a technology analyst firm. "Coverity's introduction of SAT for the static analysis of software will unlock a wealth of highly advanced logic to address these fundamental challenges and set a new standard for innovation in static analysis."

Unlike current static analysis engines that rely on dataflow analysis and multiple checkers to identify software defects, the SAT engine is based on Boolean satisfiability and will enable multiple 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 every relevant software 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 analyzed by SAT-based Solvers for the first time in commercial computer programming.

Over 300 customers rely on Coverity Prevent to analyze every path through their applications, and now, by leveraging SAT, Prevent can analyze every value in every computation within these programs. This exhaustive static code analysis enables Coverity to deliver the most accurate identification of critical performance and security vulnerabilities in the industry.

"We are committed to helping our customers create the most reliable and secure code in the world," said Ben Chelf, CTO of Coverity. "Bringing SAT’s proven capabilities to static code analysis will provide developers with an arsenal of new Solvers that uncover the toughest code defects. By leveraging technology that automates the accurate detection of defects, developers can stop wasting their valuable time tracking down bugs and can focus on bringing new software applications to market."

Available today, Coverity’s False Path Pruning Solver is the first Solver to be released for Prevent. 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 unfeasible defects. By pruning these infeasible results, the Solver increases the overall accuracy of code analysis results and allows developers to focus on defects that pose a genuine threat to the success of their projects.

After testing on over 2 million lines of code from multiple applications of open source software from Coverity’s Scan project, the False Path Pruning Solver was found to reduce false positive results by an average of 30 percent.

Coverity plans to release two additional Solvers in early 2008 that allow customers to check code assertions statically and to detect critical bug categories including integer overflows. In addition, these Solvers will expand Coverity’s existing dataflow analysis capabilities to uncover even greater numbers of buffer overflows while maintaining a low false positive rate.

Coverity Prevent is available immediately for C, C++ and Java software projects, and is priced based on project size.
A free trial of Prevent that will detect a wide range of crash-causing defects in your code base within hours is available.

This page is based on a press release of Coverity Inc.

last updated: 13.01.2009

© 2008-2009 Coverity Inc., San Francisco
Coverity Prevent, coverity Extend, Coverity Architecture Analyzer for C/C++ and Coverity Architecture Analyzer for Java are products and trademarks of Coverity, San Francisco (USA)
all other trademarks of this site are the property of their respective owners.