Write a Blog >>
Mon 10 Jul 2017 16:00 - 16:25 at Bren 1414 - Symbolic Execution Chair(s): Gordon Fraser

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 Jul

issta-2017-research
16:00 - 17:15: Technical Papers - Symbolic Execution at Bren 1414
Chair(s): Gordon FraserUniversity of Sheffield
issta-2017-research16:00 - 16:25
Talk
David Mitchel PerryPurdue University, Andrea MattavelliImperial College London, Xiangyu ZhangPurdue University, Cristian CadarImperial College London
DOI
issta-2017-research16:25 - 16:50
Talk
Wei SunUniversity of Nebraska-Lincoln, USA, Lisong XuUniversity of Nebraska-Lincoln, USA, Sebastian ElbaumUniversity of Nebraska-Lincoln, USA
DOI
issta-2017-research16:50 - 17:15
Talk
Pietro BraioneUniversity of Milano-Bicocca, Italy, Giovanni DenaroUniversity of Milano-Bicocca, Italy, Andrea MattavelliImperial College London, Mauro PezzèUniversity of Milano-Bicocca, Italy
DOI