Concurrency Verification with Maximal Path Causality Conference Paper

abstract

• 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.

name of conference

• Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

authors

• Huang, Jeff

published proceedings

• ESEC/FSE'18: PROCEEDINGS OF THE 2018 26TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING

author list (cited authors)

• Yi, Q., & Huang, J.

citation count

• 2

complete list of authors

• Yi, Qiuping||Huang, Jeff

publication date

• October 2018

publisher

• Association for Computing Machinery (ACM)  Publisher

keywords

• Concurrency
• Dynamic Symbolic Execution
• Verification

Digital Object Identifier (DOI)

• 10.1145/3236024.3236048

International Standard Book Number (ISBN) 13

• 9781450355735

start page

• 366

end page

• 376

URL

• http://dx.doi.org/10.1145/3236024.3236048