Abstract interpretation based program testing
Patrick M. Cousot, Radhia Cousot · 2000
Every one can daily experiment that programs are bugged. Software bugs can have severe if not catastrophic consequences in computer-based safety critical applications. This impels the development of formal methods, whether manual, computer-assisted or automatic, for verifying that a program satisfies a specification. Among the automatic formal methods, program static analysis can be used to check for the absence of run-time errors. In this case the specification is provided by the semantics of the programming language in which the program is written. Abstract interpretation provides a formal theory for approximating this semantics, which leads to completely automated tools where run-time bugs can be statically and safely classified as unreachable, certain, impossible or potential. We discuss the extension of these techniques to abstract testing where specifications are provided by the programmers. Abstract testing is compared to program debugging and model-checking.