{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215382},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_16","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"160-171","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":109,"title":["Experience with Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Satyaki","family":"Das","sequence":"first","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Seungjoon","family":"Park","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201. Springer-Verlag, November 1996. Palo Alto, California, November 6-8.","DOI":"10.1007\/BFb0031808"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/579.587","volume":"6","author":"M. Ben-Ari","year":"1984","unstructured":"M. Ben-Ari. Algorithms for on-the-fly garbage collection. ACM Transactions on Programming Languages and Systems, 6(3):333\u2013344, July 1984.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR3","first-page":"293","volume":"1427","author":"M. A. Col_on","year":"1998","unstructured":"M. A. Col_on and T. E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Conference on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 293\u2013304. Springer-Verlag, 1998.","journal-title":"Conference on Computer-Aided Verification"},{"issue":"11","key":"16_CR4","doi-asserted-by":"publisher","first-page":"966","DOI":"10.1145\/359642.359655","volume":"21","author":"E. W. Dijkstra","year":"1978","unstructured":"E. W. Dijkstra, L. Lamport, A. Martin, C. S. Scholten, and E. F. M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Communications of the ACM, 21(11):966\u201375, November 1978.","journal-title":"Communications of the ACM"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"D. Doligez and G. Gonthier. Portable, unobtrusive garbage collection for multi-processor systems. Proc. ACM Symp. on Principles of Programming Languages, January 1994.","DOI":"10.1145\/174675.174673"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"D. Doligez and X. Leroy. A concurrent, generational garbage collector for a multi-threaded implementation of ML. Proc. ACM Symp. on Principles of Programming Languages, January 1993.","DOI":"10.1145\/158511.158611"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. Proc. ACM Symp. on Principles of Programming Languages, 1995.","DOI":"10.1145\/199448.199468"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3), July 1992.","DOI":"10.1145\/146637.146681"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Conference on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 72\u201383. Springer-Verlag, 1997. June 1997, Haifa, Israel.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"16_CR10","unstructured":"K. Havelund. Mechanical verification of a garbage collector. Unpublished manuscript, 1996."},{"key":"16_CR11","unstructured":"K. Havelund and N. Shankar. A mechanized refinement proof for a garbage collector. Unpublished manuscript, 1997."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"D. Lessens and H. Sa\u00efdi. Automatic verification of parameterized networks of processes by abstraction. Electronic Notes of Theoretical Computer Science (ENTCS), 1997.","DOI":"10.1016\/S1571-0661(05)80429-3"},{"key":"16_CR13","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"},{"issue":"4","key":"16_CR14","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/s002240000093","volume":"31","author":"S. Park","year":"1998","unstructured":"S. Park and D. L. Dill. Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems, 31(4):355\u2013376, 1998.","journal-title":"Theory of Computing Systems"},{"issue":"1","key":"16_CR15","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF01788566","volume":"3","author":"C. Pixley","year":"1988","unstructured":"C. Pixley. An incremental garbage collection algorithm for multi-mutator systems. Distributed Computing, 3(1):41\u201350, 1988.","journal-title":"Distributed Computing"},{"issue":"4","key":"16_CR16","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF01211305","volume":"6","author":"D. M. Russinoff","year":"1994","unstructured":"D. M. Russinoff. A mechanically verified incremental garbage collector. Formal Aspects of Computing, 6(4):359\u2013390, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"16_CR17","unstructured":"A. P. Sistla and S. M. German. Reasoning with many processes. Symp. on Logic in Computer Science, Ithaca, pages 138\u2013152, June 1987."},{"issue":"4","key":"16_CR18","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0020-0190(87)90135-9","volume":"24","author":"J. Snepscheut van de","year":"1987","unstructured":"J. van de Snepscheut. Algorithms for on-the-fly garbage collection revisited. Information Processing Letters, 24(4):211\u201316, March 1987.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:06:02Z","timestamp":1586153162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}