Classifying Bugs with Interpolants

RiSE will host a talk by Martin Schäf on June 30, 2016

ABSTRACT

We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

Speaker bio:
Martin Schäf is a Computer Scientist at SRI International. Before joining SRI, he worked at the United Nations University in Macau. He received his PhD from University of Freiburg in 2011, and his MS degree in computer science from Saarland University in 2006. His research interests include static analysis, software verification, fault localization, and GUI testing.