| Software test tools boast Boolean satisfiability |
Sep. 19, 2007
Software test tools vendor Coverity claims to be shipping the first software debugger based on Boolean satisfiability. Long-used to test IC designs before sending them to the foundry, Boolean satisfiability can come much closer to testing every possible code execution path than the dynamic debuggers popular in software testing today, Coverity claims.
Coverity added the Boolean satisfiability (SAT) capabilities to its flagship Prevent SQS (software quality system) product. The initial application for the technology is to reduce "false positives," although in time, SAT could offer many additional benefits, the vendor hints.
As a "static" code analysis tool, Prevent resembles lint and its GNU knock-off, glint. Unlike dynamic tools that operate on program code as it runs, typically in conjunction with "instrumentation" like break points and tees, static tools work on source code that has not yet been compiled. Think of it as a spell-checker or grammar checker for source code.
Coverity CTO Ben Chelf commented, "Static analysis shines in embedded, where patching is more expensive. It's hard to cover all the possibilities by just running the binary. Testing teams [using dynamic testing techniques] are thrilled to get 100 percent line coverage, but that's not even close to 100 percent of the billions or trillions of possible execution paths. Our tools can identify things that are going to hit when you run the code."
Chelf said that SAT techniques have long proved effective in the EDA (electronic data automation) industry, where SAT-based tools are used to statically test integrated circuit designs before sending them to the foundry. However, SAT principles have not previously been applied to software quality testing, the vendor believes.
It works like this. The source code is parsed into a tree called a "Software DNA Map," in Coverity's marketing language. The process involves breaking down software operations into Boolean operators (AND, NOT, OR, and so on) and Boolean values (TRUE and FALSE). This takes about 150 percent as long as actually compiling the code, Chelf said.
Once built, the parse tree can be analyzed by SAT-based solvers, such as Coverity's new False Path Pruning Solver. This Solver can "determine if the path to a potential software defect is feasible," and then discard the roughly 30 percent of reported defects that turn out not to be. The payoff is output containing only about 20 percent false positives, according to Chelf.
Multiple solvers can operate on the tree concurrently, and Coverity has hinted that additional SAT-based solvers are in the wings. Such solvers might be able to find buffer, string, and integer overflows, helping testers answer that ageless debugging riddle, "Will this arithmetic operation ever go beyond the bounds of what it's able to compute?" Chelf suggested.
(Click to enlarge)
(Click to enlarge)
Chelf confirmed that Prevent and the new SAT-based solver require the use of specific compilers. However, the products support a broad range of free and commercial compilers, he said, including those from Intel, ARM, Wind River, and the GNU project.
Chelf proudly added that Coverity now has about 300 customers, including such notable device makers as printer giant HP. "HP is standardizing and deploying [our tools] to all of their development groups," he said.
In a statement, Theresa Lanowitz, founder of tech analyst firm Voke, said, "Coverity's introduction of SAT for the static analysis of software will set a new standard for innovation in static analysis."
Chelf added, "Bringing SAT's proven capabilities to static code analysis will provide developers with an arsenal of new Solvers that uncover the toughest code defects."
Availability
Coverity's Prevent SQS has been available for several years now, in C/C++ and Java editions. It was recently used in a project sponsored by the U.S. Department of Homeland security to test 250 open source projects, including Linux. Prevent also recently helped find and fix a large X Window flaw, the company says.
The False Path Pruning Solver is new to the market, but shipping now. Pricing was not disclosed.
-- Henry Kingman
Related Stories:
(Click here for further information)
|
|
|
7 Advantages of D2D Backup
For decades, tape has been the backup medium of choice. But, now, disk-to-disk (D2D) backup is gaining in favor. Learn why you should make the move in this whitepaper.
4 Legal Reasons to Control Internet Access
The Internet is obviously a valuable resource for many organizations. However, many are exposed to legal liability concerns because they fail to control Internet access. Learn if you're safe in this white paper.
Rapidly Resolve J2EE Application Problems
Whether you are in the process of building J2EE applications or have J2EE applications already running in production, you must ensure that they deliver the expected ROI. Learn how in this white paper.
Load Testing 2.0 for Web 2.0
There are many unknowns in stress testing Web 2.0 applications. Find out how to test the performance of Web 2.0 in this white paper.
Build Better Games Online
For the game infrastructure providers, life is complex. Making money from games has become more complicated. Why? Find out in this white paper.
Building a Virtual Infrastructure from Servers to Storage
This white paper discusses the virtual storage solutions that reduce cost, increase storage utilization, and address the challenges of backing up and restoring Server environments.
Gaining Faster Wireless Connections with WiMAX
Welcome to what is quickly becoming the hyperconnected world where anything that would benefit from being connected to the network will be connected. Learn more in this white paper.
Is Your Desktop a Security Threat?
The new wave of sophisticated crimeware not only targets specific companies, but also targets desktops and laptops as backdoor entryways into those business’ operations and resources. Learn how to stay safe in this white paper.
Increasing SAN Reliability by 100 Percent
Storage area networks (SAN) are a strong part of storage plans. Learn how to increase your reliability and uptime by 100 percent in this case study.
|
|
|
|
|
Use of this site is governed by our Terms of
Service and Privacy Policy.
Except where otherwise specified, the contents of this site are copyright © 1999-2008
Ziff Davis Enterprise Holdings Inc. All Rights Reserved.
Reproduction in whole or in part in any form or medium without express written permission of Ziff Davis Enterprise is
prohibited. Linux is a registered trademark of Linus Torvalds. All other marks are the property of their respective owners.
news feed