A software falsifier
Daniël Brand · 2002
A falsifier is a tool for discovering errors by static source-code analysis. Its goal is to discover them while requiring minimal programmer effort. In contrast to lint-like tools or verifiers, which try to maximize the number of errors reported at the expense of allowing "false errors", a falsifier's goal is to guarantee no false errors. To further minimize programmer effort, no specification or extra information about the program is required. That, however, does not preclude project-specific information from being built in. The class of errors that are detectable without any specification is important not only because of the low cost of detection, but also because it includes errors of portability, irreproducible behavior, etc., which are very expensive to detect by testing. This paper describes the design and implementation of such a falsifier, and reports on experience with its use for design automation software. The main contribution of this work lies in combining data-flow analysis with symbolic execution to take advantage of their relative advantages.