Automated Debugging as a Constraint Solving Problem

Event details
Date | 10.01.2017 |
Hour | 11:00 › 12:30 |
Location | |
Category | Conferences - Seminars |
by Thomas Wies - New York University
Abstract
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. In my talk, I will present new algorithms for automatically localising and explaining errors in programs. Specifically, I will present techniques for finding the sources of type errors in functional programs and for explaining safety violations in imperative programs. These techniques have in common that they leverage the recent advances in automated theorem proving to scale to realistic programs while providing formal correctness and optimality guarantees. We found that these new algorithms have the potential to significantly increase the quality of error reports produced by compilers and testing tools.
Bio
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 is recipient of an NSF CAREER Award, an OOPSLA Best Paper Award, and a Microsoft European PhD Scholarship. 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.
More information
Abstract
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. In my talk, I will present new algorithms for automatically localising and explaining errors in programs. Specifically, I will present techniques for finding the sources of type errors in functional programs and for explaining safety violations in imperative programs. These techniques have in common that they leverage the recent advances in automated theorem proving to scale to realistic programs while providing formal correctness and optimality guarantees. We found that these new algorithms have the potential to significantly increase the quality of error reports produced by compilers and testing tools.
Bio
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 is recipient of an NSF CAREER Award, an OOPSLA Best Paper Award, and a Microsoft European PhD Scholarship. 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.
More information
Practical information
- General public
- Free
- This event is internal
Organizer
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch
Contact
- Prof. Viktor Kuncak