{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:36:48Z","timestamp":1775054208322,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540401179","type":"print"},{"value":"9783540448297","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_14","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"213-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":82,"title":["Thread-Modular Model Checking"],"prefix":"10.1007","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In POPL 03: Principles of Programming Languages, pages 62\u201373. ACM Press, 2003.","DOI":"10.1145\/640128.604137"},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logic of Programs","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Workshop on Logic of Programs, Lecture Notes in Computer Science 131, pages 52\u201371. Springer-Verlag, 1981."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"J. M. Cobleigh, D. Giannakopoulou, and C. S. P\u0103s\u0103reanu. Learning assumptions for compositional verification. In TACAS 03: Tools and Algorithms for the Construction and Analysis of Systems, 2003. To appear.","DOI":"10.1007\/3-540-36577-X_24"},{"key":"14_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"ESOP 02: European Symposium on Programming","author":"C. Flanagan","year":"2002","unstructured":"C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In ESOP 02: European Symposium on Programming, Lecture Notes in Computer Science 2305, pages 262\u2013277. Springer-Verlag, 2002."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-45657-0_14","volume-title":"CAV 02: Computer Aided Verification","author":"C. Flanagan","year":"2002","unstructured":"C. Flanagan, S. Qadeer, and S. A. Seshia. A modular checker for multithreaded programs. In CAV 02: Computer Aided Verification, Lecture Notes in Computer Science 2404, pages 180\u2013194. Springer-Verlag, 2002."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"D. Giannakopoulou, C. S. P\u0103s\u0103reanu, and H. Barringer. Assumption generation for software component verification. In ASE 02: Automated Software Engineering, pages 3\u201312. IEEE Computer Society, 2002.","DOI":"10.1109\/ASE.2002.1114984"},{"key":"14_CR7","unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979."},{"issue":"1\u20132","key":"14_CR8","first-page":"41","volume":"9","author":"C. N. Ip","year":"1996","unstructured":"C. N. Ip and D. L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1\u20132):41\u201375, 1996.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"14_CR9","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":"14_CR10","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Fifth International Symposium on Programming","author":"J. Queille","year":"1981","unstructured":"J. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Fifth International Symposium on Programming, Lecture Notes in Computer Science 137, pages 337\u2013351. Springer-Verlag, 1981."},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programming Languages and Systems, 22(2):416\u2013430, 2000.","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:02:19Z","timestamp":1737172939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}