Coverity's PR counsel just forwarded me a message from Ben Chelf, clarifying his note posted Wednesday: Thanks for posting Ben Chelf's comments so quickly. Upon reading the posting, Ben realized that some of your readers may be confused by this statement: Boolean Satisfiability is the same type of technology that Synopsys, Cadence, and other EDA tools providers leverage in verifying chip designs. This new Coverity’s PR counsel just forwarded me a message from Ben Chelf, clarifying his note posted Wednesday: Thanks for posting Ben Chelf’s comments so quickly. Upon reading the posting, Ben realized that some of your readers may be confused by this statement: Boolean Satisfiability is the same type of technology that Synopsys, Cadence, and other EDA tools providers leverage in verifying chip designs. This new technology, which is called SAT, allows the analysis, not only of all the paths through the code but also all of the potential values of the variables in any given path. The technology actually isn’t new, it’s a new application of the technology Synopsys, Cadence, and other EDA tool providers have been using to find hardware defects. What is new is its application to software development. Here’s a statement that might clear this up: Synopsys, Cadence, and other EDA tools providers leverage Boolean Satisfiability (SAT) in verifying chip designs through sophisticated SAT-solvers that can solve formulas on millions of variables. The application of SAT-solvers to software analysis allows the analysis to cover not only all the paths through the code but also all the potential values of the variables in any given path. Thanks again! Software Development