Model-Checking Software Using Precise Abstractions

Formal verification techniques are not yet widely used in the software industry, perhaps because software tends to be more complex than hardware, and the penalty for bugs is often lower (software can be patched after the release). Instead, a large amount of time and money is being spent on software testing, which misses many subtle errors, espe