SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Fri 24 Oct 2014 13:52 - 14:15 at Salon E - Static Analysis Chair(s): Anders Møller

We address the problem of computing semantic differences between a program and a patched version of the program. Our goal is to obtain a precise characterization of the difference between program versions, or establish their equivalence. We focus on infinite-state numerical programs, and use abstract interpretation to compute an over-approximation of program differences.

Computing differences and establishing equivalence under abstraction requires abstracting relationships between variables in the two programs. Towards that end, we use a correlating abstract domain to compute a sound approximation of these relationships which captures semantic difference. This approximation can be computed over any interleaving of the two programs. However, the choice of interleaving can significantly affect precision. We present a speculative search algorithm that aims to find an interleaving of the two programs with minimal abstract semantic difference. This method is unique as it allows the analysis to dynamically alternate between several interleavings.

We have implemented our approach and applied it to real-world examples including patches from Git, GNU Coreutils, as well as a few handpicked patches from the Linux kernel and the Mozilla Firefox web browser. Our evaluation shows that we compute precise approximations of semantic differences, and report few false differences.

Fri 24 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
Static AnalysisOOPSLA at Salon E
Chair(s): Anders Møller Aarhus University
13:30
22m
Talk
Validation of Memory Accesses Through Symbolic Analyses
OOPSLA
Link to publication
13:52
22m
Talk
Abstract Semantic Differencing via Speculative Correlation
OOPSLA
Nimrod Partush Technion, Eran Yahav Technion
Link to publication
14:15
22m
Talk
Efficient Subcubic Alias Analysis for C
OOPSLA
Qirun Zhang The Hong Kong University of Science and Technology, A: Xiao Xiao The Hong Kong University of Science and Technology, A: Charles Zhang Hong Kong University of Science and Technology, A: Hao Yuan BOPU Technologies, A: Zhendong Su University of California, Davis
Link to publication
14:37
22m
Talk
Static Analysis for Independent App Developers
OOPSLA
Lucas Brutschy ETH Zurich, Pietro Ferrara IBM Thomas J. Watson Research Center, Peter Müller ETH Zurich
Link to publication