{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T13:56:58Z","timestamp":1789999018354,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434191","type":"print"},{"value":"9783540460022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_13","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T06:29:59Z","timestamp":1193552999000},"page":"173-187","source":"Crossref","is-referenced-by-count":43,"title":["Towards the Automated Verification of Multithreaded Java Programs"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Francois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Van Begin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS\u201996, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"Parameterized Verification of Multithreaded Software Libraries","author":"T. Ball","year":"2001","unstructured":"T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. In Proc. TACAS\u201901, LNCS 2031, pages 158\u2013173, 2001."},{"key":"13_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-58152-9_11","volume-title":"Petri Nets with marking-dependent arc multiplicity: properties and analysis","author":"G. Ciardo","year":"1994","unstructured":"G. Ciardo. Petri Nets with marking-dependent arc multiplicity: properties and analysis. In Proc. ICATPN\u201994, LNCS 815, pages 179\u2013198, 1994."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"J. C. Corbett. Constructing Compact Models of Concurrent Java Programs. In Proc. ISSTA\u201998, pages 1\u201310, 1998.","DOI":"10.1145\/271771.271778"},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-46419-0_29","volume-title":"Symbolic Representation of Upward Closed Sets","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno, and J.-F. Raskin. Symbolic Representation of Upward Closed Sets. In Proc. TACAS 2000, LNCS 1785, pages 426\u2013440, 2000."},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-44585-4_28","volume-title":"Attacking Symbolic State Explosion","author":"G. Delzanno","year":"2001","unstructured":"G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking Symbolic State Explosion. In Proc. CAV\u201901, LNCS 2102, pages 298\u2013310, 2001."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. of LICS\u2019 98), pages 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS\u201999, pages 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! TCS 256 (1\u20132):63\u201392, 2001.","journal-title":"TCS"},{"issue":"3","key":"13_CR10","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675\u2013735 (1992)","journal-title":"JACM"},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"HyTech: a Model Checker for Hybrid Systems","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a Model Checker for Hybrid Systems. In Proc. CAV\u201997, LNCS 1254, pages 460\u2013463, 1997."},{"key":"13_CR12","unstructured":"D. Lea. Concurrent Programming in Java. Design Principle and Patterns. Second Edition. The Java Series. Addison Wesley, 2000."},{"key":"13_CR13","unstructured":"D. Zampuni\u2019eris, and B. Le Charlier. Efficient Handling of Large Sets of Tuples with Sharing Trees. In Proc. DCC\u201995, 1995."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:50:26Z","timestamp":1737503426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}