Despite significant recent advances, the effectiveness of symbolic execution is limited when used to test complex, real-world software. One of the main scalability challenges is related to constraint solving: large applications and long exploration paths lead to complex constraints, often involving big arrays indexed by symbolic expressions. In this paper, we propose a set of semantics-preserving transformations for array operations that take advantage of contextual information collected during symbolic execution. Our transformations lead to simpler encodings and hence better performance in constraint solving. The results we obtain are encouraging: we show, through an extensive experimental analysis, that our transformations help to significantly improve the performance of symbolic execution in the presence of arrays. We also show that our transformations enable the analysis of new code, which would be otherwise out of reach for symbolic execution.
Mon 10 JulDisplayed time zone: Tijuana, Baja California change
16:00 - 17:15 | |||
16:00 25mTalk | Accelerating Array Constraints in Symbolic Execution Technical Papers David Mitchel Perry Purdue University, Andrea Mattavelli Imperial College London, Xiangyu Zhang Purdue University, Cristian Cadar Imperial College London DOI | ||
16:25 25mTalk | Improving the Cost-Effectiveness of Symbolic Testing Techniques for Transport Protocol Implementations under Packet Dynamics Technical Papers Wei Sun University of Nebraska-Lincoln, USA, Lisong Xu University of Nebraska-Lincoln, USA, Sebastian Elbaum University of Nebraska-Lincoln, USA DOI | ||
16:50 25mTalk | Combining Symbolic Execution and Search-Based Testing for Programs with Complex Heap Inputs Technical Papers Pietro Braione University of Milano-Bicocca, Italy, Giovanni Denaro University of Milano-Bicocca, Italy, Andrea Mattavelli Imperial College London, Mauro Pezzè University of Milano-Bicocca, Italy DOI |