Software Analysis Engine is based on Boolean satisfiability.September 27, 2007 -
Coverity Prevent SQS software analysis engine leverages software representations to automatically identify complex defects in source code. Use of Boolean satisfiability enables multiple solvers to identify defects. This method translates each relevant software operation into true, false, and, not, and or values to create bit accurate representations. Security engine comes with False Path Pruning Solver and is available for C, C++ and Java software projects.
(Archive News Story - Products mentioned in this Archive News Story may or may not be available from the manufacturer.)
Original Press release
Coverity, Inc.
185 Berry St. Suite 3600
San Francisco, CA, 94107
USA
Coverity Announces Breakthrough Software Code Analysis Engine
World's First Use of Satisfiability to Accelerate Software Development Now Available in Coverity Prevent SQS
BOSTON, Sept. 19 -- EMBEDDED SYSTEMS CONFERENCE (ESC) -- Coverity, Inc., the leader in improving software quality and security, today announced the first software analysis engine based on Boolean satisfiability (SAT). Coverity's SAT engine leverages a highly accurate representation of software, the 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 SQS accelerates companies' ability 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, 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 SAT-based Solvers to analyze source code for the first time in commercial computer programming.
Over 300 customers rely on Coverity Prevent SQS to analyze every path through their applications, and now, by leveraging SAT, Prevent SQS 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 focus instead on bringing new software applications to market."
Available today, Coverity's False Path Pruning Solver is the first Solver to be released for Prevent SQS. The False Path Pruning Solver significantly lowers the number of false positive results in static code analysis. Leveraging SAT to determine if the path to a potential software defect is feasible, the Solver identifies and excludes unfeasible defects. By 'pruning' these unfeasible 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 being tested 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 shown to reduce false positive results by an average of 30%.
Coverity plans to release two additional Solvers in early 2008 that will 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.
Pricing and Availability
Coverity Prevent SQS is available immediately for C, C++ and Java software projects, and is priced based on project size. For more information, visit http://www.coverity.com/.
About Coverity
Coverity (http://www.coverity.com/), the leader in improving software quality and security, is a privately held company headquartered in San Francisco. Coverity's groundbreaking technology removes the barriers to writing and delivering complex software by automatically finding and helping to fix critical software defects and security vulnerabilities as the software is written. More than 300 leading companies choose Coverity because it scales to tens of millions of lines of code, has the lowest false positive rate and provides 100% path coverage. Companies like Juniper Networks, Symantec, McAfee, Synopsys, Palm and Wind River work with Coverity's tools to find and fix security and quality defects from their mission-critical code.
Source: Coverity, Inc. CONTACT: Jim Shissler, Director of Public Relations of Coverity,
+1-415-694-5342, jshissler@coverity.com; or Patricia Colby of Page One
+PR, 1-415-875-7494, patricia@pageonepr.com, for Coverity, Inc. Web site: http://www.coverity.com/
|
|
|
|
|
|
|
| 
