UC Santa Cruz
Modular Verification of Multithreaded Programs
- Author(s): Flanagan, Cormac
- Freund, Stephen N.
- Qadeer, Shaz
- Seshia, Sanjit A.
- et al.
Published Web Locationhttps://doi.org/10.1016/j.tcs.2004.12.006
Multithreaded software systems are prone to errors due to the difficulty of reasoning about multiple interleaved threads operating on shared data. Static checkers that analyze a program's behavior over all execution paths and all thread interleavings are a powerful approach to identifying bugs in such systems. In this paper, we present Calvin, a scalable and expressive static checker for multithreaded programs based on automatic theorem proving. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. Our experience applying Calvin to several real-world programs indicates that Calvin has a moderate annotation overhead and can catch common defects in multithreaded programs, such as synchronization errors and violations of data invariants.
Many UC-authored scholarly publications are freely available on this site because of the UC Academic Senate's Open Access Policy. Let us know how this access is important for you.