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

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00
Symbolic Execution and Constraint SolvingResearch Papers at Horizons 10-11
Chair(s): Satish Chandra Facebook
15:30
22m
Talk
Concurrency Verification with Maximal Path Causality
Research Papers
Qiuping Yi Texas A&M University, Jeff Huang Texas A&M University
15:52
22m
Talk
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Research Papers
Shengjian (Daniel) Guo Virginia Tech, Meng Wu Virginia Tech, Chao Wang USC
16:15
22m
Talk
Symbolic Execution with Existential Second-Order Constraints
Research Papers
Sergey Mechtaev National University of Singapore, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler, Abhik Roychoudhury National University of Singapore
DOI Pre-print
16:37
22m
Talk
Parameterized Model Counting for String and Numeric Constraints
Research Papers
Abdulbaki Aydin Microsoft, USA, William Eiers University of California at Santa Barbara, USA, Lucas Bang , Tegan Brennan , Miroslav Gavrilov University of California at Santa Barbara, USA, Tevfik Bultan University of California, Santa Barbara, Fang Yu National Chengchi University