Automated Debugging as a Constraint Solving Problem

Опубликовано 27 июня 2016, 20:48

Debugging is one of the most time consuming aspects of software development. Any automation that reduces the manual effort involved in this task can have a significant impact on software productivity. An integral part of all debugging activities is error localization: once undesired behavior is spotted, the actual defect has to be identified before a fix can be developed. Most existing fault localization techniques rely on the availability of high quality test suites, which limits their applicability in practice. It therefore seems necessary to explore alternatives that complement testing-based techniques. We will present two novel algorithms that reduce the problem of error localization to constraint solving. The first algorithm can be used for slicing error traces and explaining code inconsistencies in imperative programs. The second algorithm finds the best explanations of type errors in functional programs. The reduction to constraint solving leverages the recent advances in automated theorem proving to localize errors without relying on testing. Moreover, it can provide formal quality guarantees about the computed results. Our experiments indicate that our new algorithms have the potential to significantly increase the quality of error reports produced by compilers and debugging tools. The talk will be split into two parts presented by Thomas Wies and Zvonimir Pavlinovic.