Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Fri 4 Nov 2016 14:45 - 15:10 at Matterhorn 1 - Bug Detection Analysis and Model Checking Chair(s): Ben Livshits

<p>Bounded model checking based debugging solutions search for mutations of program expressions that produce the expected output for a currently failing test. However, the current localization tools are not <i>regression aware</i>: they do not use information from the passing tests in their localization formula. On the other hand, the current repair tools attempt to guarantee <i>regression freedom</i>: when provided with a set of passing tests, they guarantee that none of these tests can break due to the suggested repair patch, thereby constructing a large repair formula.</p>

<p>In this paper, we propose <i>regression awareness</i> as a means to improve the quality of localization and to scale repair. To enable regression awareness, we summarize the proof of correctness of each passing test by computing Craig Interpolants over a symbolic encoding of the passing execution, and use these summaries as additional soft constraints while synthesizing altered executions corresponding to failing tests. Intuitively, these additional constraints act as roadblocks, thereby discouraging executions that may damage the proof of a passing test. We use a partial MAXSAT solver to relax the proofs in a systematic way, and use a ranking function that penalizes mutations that damage the existing proofs.</p>

<p>We have implemented our algorithms into a tool, TINTIN, that enables <i>regression aware</i> localization and repair. For localizations, our strategy is effective in extracting a superior ranking of suspicious locations: on a set of 52 different versions across 12 different programs spanning three benchmark suites, TINTIN achieves a saving of developer effort by almost 45% (in terms of the locations that must be examined by a developer to reach the ground-truth repair) in the worst case and 27% in the average case over existing techniques. For automated repairs, on our set of benchmarks, TINTIN achieves a 2.3X speedup over existing techniques without sacrificing much on the ranking of the repair patches: the ground-truth repair appears as the topmost suggestion in more than 70% of our benchmarks.</p>

Fri 4 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10
Bug Detection Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Ben Livshits Microsoft Research
13:30
25m
Talk
Finding Compiler Bugs via Live Code Mutation
OOPSLA
Chengnian Sun University of California, Davis, Vu Le Microsoft, Zhendong Su University of California, Davis
DOI Media Attached
13:55
25m
Talk
Finding Resume and Restart Errors in Android Applications
OOPSLA
Zhiyong Shan University of Central Missouri, USA, Tanzirul Azim University of California at Riverside, USA, Iulian Neamtiu New Jersey Institute of Technology, USA
DOI Pre-print
14:20
25m
Talk
Low-Overhead and Fully Automated Statistical Debugging with Abstraction RefinementAEC
OOPSLA
Zhiqiang Zuo University of California, Irvine, Lu Fang University of California, Irvine, Siau-Cheng Khoo , Harry Xu University of California, Irvine, Shan Lu University of Chicago
DOI Media Attached
14:45
25m
Talk
To Be Precise: Regression Aware Debugging
OOPSLA
Rohan Bavishi IIT Kanpur, India, Awanish Pandey IIT Kanpur, India, Subhajit Roy IIT Kanpur, India
DOI