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 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
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 22mTalk | Concurrency Verification with Maximal Path Causality Research Papers | ||
15:52 22mTalk | Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks Research Papers | ||
16:15 22mTalk | 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 22mTalk | 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 |