Abstract interpretation is a formal method that enables the static determination (i.e. at compile-time) of the dynamic properties (i.e. at run-time) of programs. So far, this method has mainly been used to build sophisticated, optimizing compilers. In this paper, we show how abstract interpretation techniques can be used to perform, prior to their execution, a static and automatic debugging of imperative programs. This novel approach, which we call abstract debugging, lets programmers use assertions to express invariance properties as well as inevitable properties of programs, such as termination. We show how such assertions can be used to find the origin of bugs, rather than their occurrences, and determine necessary conditions of program correctness, that is, necessary conditions for programs to be bug-free and correct with respect to the programmer's assertions. We also show that assertions can be used to restrict the control-flow of a program and examine its behavior along specific execution paths and find necessary conditions for the program to reach a particular point in a given state. Finally, we present the Syntox system that enables the abstract debugging of Pascal programs by the determination of the range of scalar variables, and discuss implementation, algorithmic and complexity issues.
[PostScript, PDF, Software]