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: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00: Symbolic Execution and Constraint SolvingResearch Papers at Horizons 10-11
Chair(s): Satish ChandraFacebook
15:30 - 15:52
Concurrency Verification with Maximal Path Causality
Research Papers
Qiuping YiTexas A&M University, Jeff HuangTexas A&M University
15:52 - 16:15
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Research Papers
Shengjian (Daniel) GuoVirginia Tech, Meng WuVirginia Tech, Chao WangUSC
16:15 - 16:37
Symbolic Execution with Existential Second-Order Constraints
Research Papers
Sergey MechtaevNational University of Singapore, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler, Abhik RoychoudhuryNational University of Singapore
DOI Pre-print
16:37 - 17:00
Parameterized Model Counting for String and Numeric Constraints
Research Papers
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