Automated Debugging as a Constraint Solving Problem

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.

Speaker Details

Thomas Wies is an Assistant Professor in the Computer Science Department at New York University and a member of the Analysis of Computer Systems Group in the Courant Institute of Mathematical Sciences. He received his doctorate in Computer Science from the University of Freiburg, Germany (2009). Before joining NYU in 2011, Wies held post-doctoral positions at École Polytechnique Fédérale de Lausanne, Switzerland and at the Institute of Science and Technology Austria. His research interests are in Programming Languages and Formal Methods. In particular, he is interested in the theory and development of tools that increase software productivity and assist programmers in building reliable software.

Zvonimir Pavlinovic is a second year Phd student in Computer Science at New York University advised by Thomas Wies. He is mainly interested in theoretical as well as practical problems in programming languages, currently focusing on the problem of localizing type errors in programs written in functional programming languages. He obtained his bachelor and master degree in Computer Science at University of Zagreb, Croatia after which he spent two years as a research intern at UC Berkeley working with Dawn Song on browser security topics.