Notify me of new papers
via Email or RSS

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.

SUGGESTED CITATION:
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, and Sanjit A. Seshia, "Modular Verification of Multithreaded Programs" (2004). Theoretical Computer Science. 338 (2005), pp. 153-183. 10.1016/j.tcs.2004.12.006. Postprint available free at: http://repositories.cdlib.org/postprints/1684

REQUIRED PUBLISHER STATEMENT:
The published version of this article is available at: http://www.elsevier.com/wps/find/journaldescription.cws_home/505625/description