Finding bugs in software is no easy task. One of the most popular methods is something known as static-code analysis, which typically involves a data-flow analysis that looks for defects along a code path. The problem is that data-flow analysis on its own can potentially yield false positives.

Code-analysis vendor Coverity claims to have a solution for lowering false positives and finding even more bugs. The key is seeing whether variables and equations can be solved, which could ultimately lead to a revolution in how software bugs are validated.

"With data-flow analysis we're able to get 100 percent path coverage, analyzing all the paths through code," said Ben Chelf, CTO of Coverity. "With this new technology based on Boolean satisfiability we'll be able to also get 100 percent value coverage so we'll be able to dig into all the possible variables and values along the path."

Whereas traditional static-code analysis has checkers that validate code, with Boolean satisfiability there are solvers, as the notion is all about solving formulas.

Chelf said that Boolean satisfiability asks if a given formula is satisfiable. A formula could consist of variables that can be either true or false and a developer uses "and," "or" and "not" as the operations on them.

So for example the developer says: X and Y or not Z. If the formula is satisfiable it means there is a way that the developer can assign values so that the whole expression evaluates to "True."

"The biggest source of false positives for any data-flow analysis is a path that can't actually exist when you run the code," Chelf said. "What we're now able to do is plug all the conditions that would lead to a bug report into the SAT solver and then ask if it's actually possible to satisfy the path."

The idea is for developers to spend less time on false bugs, as well as making code analysis more precise.

Though Coverity is officially announcing the technology today, it has tested it among its users, specifically those open source projects that it analyzes for code defects as part of a multi-year agreement with the Department of Homeland Security (DHS). Chelf claimed that, as a result of using the SAT solver on the DHS open source projects, they have been able to reduce the false-positive rate by 30 percent.

That's not to say that Coverity had a high false-positive rate before. According to Chelf, without SAT, four out of five bugs are valid, while with SAT, nine out of 10 bugs are valid.

"From a philosophical point of view we have always hung our hat on the low false-positive rate," Chelf said. "The reason why SAT is important is not just false positives, though that's a great first application for it. But it's also going to open up a world of new defects. For us we're always trying to find as many defects as possible with the lowest false-positive rate."