Skip to main content
eScholarship
Open Access Publications from the University of California

Modular Verification of Multithreaded Programs

  • Author(s): Flanagan, Cormac
  • Freund, Stephen N.
  • Qadeer, Shaz
  • Seshia, Sanjit A.
  • et al.
Abstract

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.

Main Content
Current View