Thursday, December 20, 2012
Speaker: Thomas Dillig and Isil Dillig
Venue: IST Austria
When program veriﬁcation tools fail to verify a program, either theprogram is buggy or the report is a false alarm. In this situation, theburden is on the user to manually classify the report, but this taskis time-consuming, error-prone, and does not utilize facts alreadyproven by the analysis. We present a new technique for assistingusers in classifying error reports. Our technique computes small,relevant queries presented to a user that capture exactly the information the analysis is missing to either discharge or validate the error. Our insight is that identifying these missing facts is an instanceof the abductive inference problem in logic, and we present a newalgorithm for computing the smallest and most general abductionsin this setting. We perform the ﬁrst user study to rigorously evaluatethe accuracy and effort involved in manual classiﬁcation of error reports. Our study demonstrates that our new technique is very usefulfor improving both the speed and accuracy of error report classiﬁcation.