|
Description: The objective of this research is to
develop automated static and runtime analysis techniques for detecting and mitigating
bugs in concurrent systems, e.g., low-level systems code and implementations
of concurrent data structures. Concurrent software in general and concurrent
data structures in particular are becoming widespread in multi-core and
distributed computing environments. However, they are difficult to design and
analyze due to the often astronomically large number of thread interleavings.
We are developing algorithms and software tools to help programmers analyze
and debug these applications.
Publications:
- "Round-Up: Runtime verification of quasi
linearizability for concurrent data structures," Lu Zhang, Arijit Chattopadhyay, and Chao Wang. IEEE
Transactions on Software Engineering (TSE). 2015. (expansion of our
ASE13 paper)
- "Verifying a quantitative relaxation of
linearizability via refinement," Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang. International Journal on Software
Tool and Technology Transfer (STTT). 2015. (expansion of our SPIN13
paper)
- "Round-Up:
Runtime checking quasi linearizability of concurrent data structures,"
Lu Zhang, Arijit Chattopadhyay, and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering
(ASE'13). Palo Alto, CA. 2013.
- "Verifying a quantitative relaxation of linearizability
via refinement," Kiran Adhikari,
James Street, Chao Wang, Yang Liu and Shaojie
Zhang. International SPIN Symposium on Model Checking of Software
(SPIN'13). Stony Brook, NY. 2013. (journal version)
Benchmarks:
|