Algorithmic program debugging. Algorithmic debugging (also called declarative debugging) is a debugging technique that compares the results of sub-computations with what the programmer intended. The technique constructs an internal representation of all computations and sub-computations performed during the execution of a buggy program and then asks the programmer about the correctness of such computations. By asking the programmer questions or using a formal specification, the system can identify precisely where in a program a bug is located. Debugging techniques can dramatically reduce the time and effort spent on debugging.

Overview

Program debugging is an extremely common part of software development. Until the 1980s the craft of program debugging, practiced by every programmer, was without any theoretical foundation. In the early 1980s, systematic and principled approaches to program debugging were developed. In general, a bug occurs when a programmer has a specific intention regarding what the program should do, yet the program actually written exhibits a different behavior than intended in a particular case. 
One way of organizing the debugging process is to automate it (at least partially) via an algorithmic debugging technique. The idea of algorithmic debugging is to have a tool that guides the programmer along the debugging process interactively: It does so by asking the programmer about possible bug sources. 
The algorithmic debugging technique constructs an internal representation of all computations and sub-computations performed during the execution of a buggy program (an execution tree). Then, it asks the programmer about the correctness of such computations. The programmer answers "YES" when the result is correct or "NO" when the result is wrong. Some algorithmic debuggers also accept the answer "I don't know" when the programmer cannot give an answer (e.g., because the question is too complex). Thus, the answers of the programmer guide the search for the bug until it is isolated by discarding correct parts of the program. The algorithmic debugging process finds one bug at a time. In order to find different bugs, the process should be restarted again for each different bug.

Origins, current and future directions

Algorithmic debugging was first developed by Ehud Shapiro during his PhD research at Yale University, as introduced in his PhD thesis, selected as a 1982 ACM Distinguished Dissertation. Shapiro implemented the method of algorithmic debugging in Prolog (a general purpose logic programming language) for the debugging of logic programs. In case of logic programs, the intended behavior of the program is a model (a set of simple true statements) and bugs are manifested as program incompleteness (inability to prove a true statement) or incorrectness (ability to prove a false statement). The algorithm would identify a false statement in the program and provide a counter-example to it or a missing true statement that it or its generalization should be added to the program. A method to handle non-termination was also developed. 
The research and development in the field of algorithmic debugging has made major improvements over the original algorithms for debugging Prolog and other and extended the ideas to other language paradigms such as functional languages and object oriented languages.
Three decades since its introduction, algorithmic debugging is still an active field of computer science research  and will probably remain so for decades as no panacea is in sight.

References

Debugging