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

We present a technique that systematically explores the state spaces of concurrent programs across both the schedule space and the input space. The cornerstone is a new model called Maximal Path Causality (MPC), which captures all combinations of thread schedules and program inputs that reach the same path as one equivalency class, and generates a unique schedule+input combination to explore each path. Moreover, the exploration for different paths can be easily parallelized. Our extensive evaluation on both popular concurrency benchmarks and real-world C/C++ applications shows that MPC significantly improves the performance of existing techniques.

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