Software falsifier

Abstract

A falsifier is a tool for discovering errors by static source-code analysis. Its goal is to discover them while requiring minimal programmer's 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', falsifier's goal is to guarantee no false errors. To further minimize programmer's effort, no specification or extra information about his program is required. That, however, does not preclude project specific information from being built in. The class of errors 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 the 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.