Concurrency Verification with Maximal Path Causality | Conference Paper individual record

© 2018 Association for Computing Machinery. 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.

author list (cited authors)
Yi, Q., & Huang, J.
publication date
ACM Press Publisher
  • Dynamic Symbolic Execution
  • Verification
  • Concurrency
citation count