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.

Spread the word: digg this story

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

---

 
This article was originally published on LinuxDevices.com and has been donated to the open source community by QuinStreet Inc. Please visit LinuxToday.com for up-to-date news and articles about Linux and open source.