{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:04:55Z","timestamp":1748070295433},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_12","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T11:50:47Z","timestamp":1184586647000},"page":"158-173","source":"Crossref","is-referenced-by-count":27,"title":["Parameterized Verification of Multithreaded Software Libraries"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cerans, B. Jonsson, and T. Yih-Kuen. General decidability theorems for infinite-state systems. LICS\u2019 96: 11th IEEE Symp. Logic in Computer Science, pages 313\u2013321, July 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"12_CR2","unstructured":"P. A. Abdulla and B. Jonsson. Ensuring completeness of symbolic verificatiom methods for infinite-state systems. Theoretical Computer Science, 1997."},{"key":"12_CR3","unstructured":"Thomas Ball, Sagar Chaki, and Sriram K. Rajamani. Parameterized verification of multithreaded software libraries. Technical Report MSRTR-2000-116, Microsoft Research, December 2000."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN 00: SPIN Workshop","author":"T. Ball","year":"2000","unstructured":"T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. SPIN 00: SPIN Workshop, Lecture Notes in Computer Science 1885, pages 113\u2013130. Springer-Verlag, 2000."},{"key":"12_CR5","unstructured":"T. Ball and S. K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research, February 2000."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. ICSE 2000: International Conference on Software Engineering, 2000.","DOI":"10.1145\/337180.337234"},{"key":"12_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"CAV 00: Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. CAV 00: Computer Aided Verification, Lecture Notes in Computer Science 1855, pages 53\u201368. Springer-Verlag, 2000."},{"issue":"3","key":"12_CR8","first-page":"143","volume":"30","author":"J. Esparza","year":"1994","unstructured":"J. Esparza and M. Nielsen. Decibility issues for petri nets-a survey. Journal of Informatik Processing and Cybernetics, 30(3):143\u2013160, 1994.","journal-title":"Journal of Informatik Processing and Cybernetics"},{"key":"12_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"CAV 96: Computer Aided Verification","author":"E. A. Emerson","year":"1996","unstructured":"E. A. Emerson and K. S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. CAV 96: Computer Aided Verification, Lecture Notes in Computer Science 1102, pages 87\u201398. Springer-Verlag, 1996."},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144\u2013179, 1990.","journal-title":"Information and Computation"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"A. Finkel. The minimal coverability graph for petri nets. Advances in Petri Nets, Lecture Notes in Computer Sceince, 674:210\u2013243, 1993.","DOI":"10.1007\/3-540-56689-9_45"},{"key":"12_CR12","unstructured":"A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 2000. To appear."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. JACM, 39(3), July 1992.","DOI":"10.1145\/146637.146681"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger. Model checking Java programs using JavaPathFinder. STTT: International Journal on Software Tools for Technology Transfer, 2(4), April 2000.","DOI":"10.1007\/s100090050043"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R. M. Karp","year":"1969","unstructured":"R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147\u2013195, 1969.","journal-title":"Journal of Computer and System Sciences"},{"key":"12_CR16","unstructured":"R. J. Lipton. The reachability problem requires exponential space. Technical report, Department of Computer Science, Yale University, 1976."},{"key":"12_CR17","unstructured":"K.L. McMillan. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil ."},{"key":"12_CR18","unstructured":"C. Petri. Fundamentals of a theory of asynchronous information flow. Information Processing 62, Proceedings of the 1962 IFIP Congress, pages 386\u2013390, 1962."},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"C. Rackoff. The covering and boundedness problem for vector addition systems. Theoretical Computer Science, 6:223\u2013231, 1978.","journal-title":"Theoretical Computer Science"},{"key":"12_CR20","unstructured":"G. Ramalingam. Context sensitive synchronization sensitive analysis is undecidable. Technical Report RC21493, IBM T.J.Watson Research, May 1999."}],"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-45319-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:09:34Z","timestamp":1556665774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}