Checking Concise Specifications for Multithreaded Software.
Stephen N. Freund, Shaz Qadeer · The Journal of Object Technology · 2004
Ensuring the reliability of multithreaded software systems is difficult due to the potential for subtle interactions between threads.We present a new modular verification technique to check concise specifications of large multithreaded programs.Our analysis scales to systems with large numbers of procedures and threads.We achieve thread-modular analysis by annotating each shared variable by an access predicate that summarizes the condition under which a thread may access that variable.We achieve procedure-modular analysis by annotating each procedure with a specification related to its implementation by an abstraction relation combining the notions of simulation and reduction.We have implemented our analysis in Calvin-R, a static checker for multithreaded Java programs.