Chao Wang    

 Project: ConcBugAssist



Description: Programmers often have to spend a significant amount of time inspecting the software code and execution traces to identify the cause of a bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between threads and the often astronomical number of interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis and repair of concurrency bugs. Both diagnosis and repair are formulated as constraint solving problems. We leverage the power of a bounded model checker (CBMC) and a max- satisfiability (MAX-SAT) solver to perform semantic analysis of the sequential computation as well as the thread interactions. The method is designed for handling critical software with small to medium code size, but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures.





  • The tar-ball (of the tool/benchmarks) we submitted for the artifact evaluation