Wed 7 Nov 2018 16:15 - 16:37 at Horizons 10-11 - Symbolic Execution and Constraint Solving Chair(s): Satish Chandra

Symbolic execution systematically explores program paths by solving path conditions. Typically, the symbolic variables range over numbers, arrays and strings. In this work, we introduce symbolic execution with existential second-order constraints — an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.

Wed 7 Nov
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

15:30 - 17:00: Research Papers - Symbolic Execution and Constraint Solving at Horizons 10-11
Chair(s): Satish ChandraFacebook
fse-2018-research-papers15:30 - 15:52
Qiuping YiTexas A&M University, Jeff HuangTexas A&M University
fse-2018-research-papers15:52 - 16:15
Shengjian (Daniel) GuoVirginia Tech, Meng WuVirginia Tech, Chao WangUSC
fse-2018-research-papers16:15 - 16:37
Sergey MechtaevNational University of Singapore, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler, Abhik RoychoudhuryNational University of Singapore
DOI Pre-print
fse-2018-research-papers16:37 - 17:00
Abdulbaki AydinMicrosoft, USA, William EiersUniversity of California at Santa Barbara, USA, Lucas Bang, Tegan Brennan, Miroslav GavrilovUniversity of California at Santa Barbara, USA, Tevfik BultanUniversity of California, Santa Barbara, Fang YuNational Chengchi University