Ensuring the reliability of multithreaded software systems isdifficult due to the interaction between threads. This paper describes the design and implementation of a static checker for such systems. To avoid considering all possible thread interleavings, the checker uses assumeguarantee reasoning, and relies on the programmer to specify an environment assumption that constrains the interaction between threads.Using this environment assumption, the checker reduces the verification of the original multithreaded program to the verification of several sequential programs, one for each thread. These sequential programs are subsequently analyzed using extended static checking techniques (basedon verification conditions and automatic theorem proving). Experience indicates that the checker is capable of handling a range of synchronization disciplines. In addition, the required environment assumptions are simple and intuitive for common synchronization idioms.
CITATION STYLE
Flanagan, C., Freund, S. N., & Qadeer, S. (2002). Thread-modular verification for shared-memory programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2305, pp. 262–277). Springer Verlag. https://doi.org/10.1007/3-540-45927-8_19
Mendeley helps you to discover research relevant for your work.