{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:30:35Z","timestamp":1775053835178,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540433637","type":"print"},{"value":"9783540459279","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45927-8_19","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T09:39:04Z","timestamp":1192786744000},"page":"262-277","source":"Crossref","is-referenced-by-count":42,"title":["Thread-Modular Verification for Shared-Memory Programs"],"prefix":"10.1007","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen N.","family":"Freund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"19_CR1","unstructured":"K. Arnold and J. Gosling. The Java Programming Language. Addison-Wesley, 1996."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Reactive modules. In Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 207\u2013218. IEEE Computer Society Press, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"19_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"CAV 98: Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, and S. Tasiran. Mocha: Modularity in model checking. In A. Hu and M. Vardi, editors, CAV 98: Computer Aided Verification, LNCS 1427, pages 521\u2013525. Springer-Verlag, 1998."},{"issue":"3","key":"19_CR4","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507\u2013534, 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"E. Abraham-Mumm and F. S. de Boer. Proof-outlines for threads in java. In CONCUR 2000: Theories of Concurrency, 2000.","DOI":"10.1007\/3-540-44618-4_18"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"E.A. Ashcroft","year":"1975","unstructured":"E.A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10:110\u2013135, January 1975.","journal-title":"Journal of Computer and System Sciences"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporallogic specifications. In Proceedings of the 16th Annual Symposium on Theory of Computing, pages 51\u201363. ACM Press, 1984.","DOI":"10.1145\/800057.808665"},{"key":"19_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60043-4_64","volume-title":"Algebraic Methodology and Software Technology","author":"P. Collette","year":"1995","unstructured":"P. Collette and E. Knapp. Logical foundations for compositional verification and development of concurrent programs in Unity. In Algebraic Methodology and Software Technology, LNCS 936, pages 353\u2013367. Springer-Verlag, 1995."},{"key":"19_CR9","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley Publishing Company, 1988."},{"key":"19_CR10","unstructured":"M. Dwyer, J. Hatcli., R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finitestate verification. In Proceedings of the 23rd International Conference on Software Engineering, 2001."},{"issue":"8","key":"19_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"E.W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation of programs. Communications of the ACM, 18(8):453\u2013457, 1975.","journal-title":"Communications of the ACM"},{"key":"19_CR12","unstructured":"D. L. Detlefs, K. R. M. Leino, C. G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December 1998."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of European Symposium on Programming, pages 91\u2013108, March 1999.","DOI":"10.1007\/3-540-49099-X_7"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S.N. Freund. Type-based race detection for Java. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 219\u2013232, 2000.","DOI":"10.1145\/349299.349328"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S.N. Freund. Detecting race conditions in large programs. In Workshop on Program Analysis for Software Tools and Engineering, pages 90\u201396, June 2001.","DOI":"10.1145\/379605.379687"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"C. Flanagan, K.R.M. Leino, M. Lillibridge, C.G. Nelson, J.B. Saxe, and R. Stata. Extended static checking for Java. Research Report 178, Compaq Systems Research Center, February 2002.","DOI":"10.1145\/512557.512558"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"C. Flanagan, S. Qadeer, and S. Seshia. A modular checker for multithreaded programs. Technical Note 02-001, Compaq Systems Research Center, 2002.","DOI":"10.1007\/3-540-45657-0_14"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"C. Flanagan and J.B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages, pages 193\u2013205. ACM, January 2001.","DOI":"10.1145\/373243.360220"},{"issue":"4","key":"19_CR19","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. B. Jones","year":"1983","unstructured":"C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596\u2013619, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR20","unstructured":"C.B. Jones. Specification and design of (parallel) programs. In R. Mason, editor, Information Processing, pages 321\u2013332. Elsevier Science Publishers B. V. (North-Holland), 1983."},{"key":"19_CR21","series-title":"Lect Notes Comput Sci","first-page":"361","volume-title":"Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness","author":"B. Jonsson","year":"1989","unstructured":"B. Jonsson. On decomposing and refining specifications of distributed systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, Lecture Notes in Computer Science 430, pages 361\u2013385. Springer-Verlag, 1989."},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125\u2013143, 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/42190.42348","volume":"10","author":"L. Lamport","year":"1988","unstructured":"L. Lamport. Control predicates are better than dummy variables. ACM Transactions on Programming Languages and Systems, 10(2):267\u2013281, April 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"19_CR24","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium, pages 280\u2013301, 2000.","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"19_CR26","unstructured":"K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. In Bart Jacobs, Gary T. Leavens, Peter M\u00fcller, and Arnd Poetzsch-Heffter, editors, Formal Techniques for Java Programs, Technical Report 251. Fernuniversit\u00e4t Hagen, May 1999."},{"issue":"4","key":"19_CR27","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"SE-7","author":"J. Misra","year":"1981","unstructured":"J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417\u2013426, 1981.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"CAV 97: Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"K.L. McMillan. A compositional rule for hardware design refinement. In O. Grumberg, editor, CAV 97: Computer Aided Verification, Lecture Notes in Computer Science 1254, pages 24\u201335. Springer-Verlag, 1997."},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"A. Mokkedem and D. Mery. On using a composition principle to design parallel programs. In Algebraic Methodology and Software Technology, pages 315\u2013324, 1993.","DOI":"10.1007\/978-1-4471-3227-1_33"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"19_CR31","unstructured":"C. G. Nelson. Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center, 1981."},{"issue":"4","key":"19_CR32","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"19_CR33","series-title":"Lect Notes Comput Sci","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C.S. P\u0103s\u0103reanu","year":"1999","unstructured":"C.S. P\u0103s\u0103reanu, M.B. Dwyer, and M. Huth. Assume-guarantee model checking of software: A comparative case study. In Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science 1680, 1999."},{"issue":"4","key":"19_CR34","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"S. Savage, M. Burrows, C.G. Nelson, P. Sobalvarro, and T.A. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391\u2013411, 1997.","journal-title":"ACM Transactions on Computer Systems"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Conference Record of the Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 105\u2013118, 1999.","DOI":"10.1145\/292540.292552"},{"key":"19_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"A proof technique for rely\/guarantee properties","author":"E.W. Stark","year":"1985","unstructured":"E.W. Stark. A proof technique for rely\/guarantee properties. In Proceedings of the 5th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 206, pages 369\u2013391. Springer-Verlag, 1985."},{"key":"19_CR37","unstructured":"N. Sterling. WARLOCK \u2014 a static data race analysis tool. In USENIX Technical Conference Proceedings, pages 97\u2013106, Winter 1993."},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"C.A. Thekkath, T. Mann, and E.K. Lee. Frangipani: A scalable distributed file system. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, pages 224\u2013237, October 1997.","DOI":"10.1145\/268998.266694"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the 28th Symposium on Principles of Programming Languages, pages 27\u201340, January 2001.","DOI":"10.1145\/360204.360206"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45927-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:29:03Z","timestamp":1556918943000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45927-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433637","9783540459279"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-45927-8_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}