{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:32:09Z","timestamp":1726407129296},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540679011"},{"type":"electronic","value":"9783540446125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44612-5_57","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T09:28:20Z","timestamp":1178357300000},"page":"619-628","source":"Crossref","is-referenced-by-count":8,"title":["Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Leonor Prensa","family":"Nieto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"57_CR1","unstructured":"Isabelle homepage. \n                    \n                      http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/isabelle.html\n                    \n                    \n                  ."},{"key":"57_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 Toplas, 6:333\u2013344, 1984.","journal-title":"ACM Toplas"},{"key":"57_CR3","unstructured":"G. Bruns. Distributed Systems Analysis with CCS Prentice-Hall, 1997."},{"key":"57_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"CAV\u2019 99","author":"S. Das","year":"1999","unstructured":"S. Das, D. L. Dill and S. Park. Experience with predicate abstraction. In CAV\u2019 99, LNCS 1633, 160\u2013171, 1999."},{"issue":"11","key":"57_CR5","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. J. 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\u2013975, 1978.","journal-title":"Communications of the ACM"},{"key":"57_CR6","unstructured":"K. Havelund. Mechanical verification of a garbage collector. FMPPTA\u201999. Available at \n                    \n                      http:\/\/ic-www.arc.nasa.gov\/ic\/projects\/amphion\/people\/havelund\/\n                    \n                    \n                  ."},{"key":"57_CR7","first-page":"1","volume":"3","author":"K. Havelund","year":"1997","unstructured":"K. Havelund and N. Shankar. A mechanized refinement proof for a garbage collector. Formal Aspects of Computing, 3:1\u201328, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"57_CR8","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF02277666","volume":"5","author":"J. E. Jonker","year":"1992","unstructured":"J. E. Jonker. On-the-fly garbage collection for several mutators. Distributed Computing, 5:187\u2013199, 1992.","journal-title":"Distributed Computing"},{"key":"57_CR9","unstructured":"T. Nipkow. Isabelle\/HOL. The Tutorial, 1998. Unpublished Manuscript. Available at \n                    \n                      http:\/\/www.in.tum.de\/~nipkow\/pubs\/HOL.html\n                    \n                    \n                  ."},{"key":"57_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"FASE\u201999","author":"T. Nipkow","year":"1999","unstructured":"T. Nipkow and L. Prensa Nieto. Owicki\/Gries in Isabelle\/HOL. In FASE\u201999, LNCS 1577, 188\u2013203. Springer-Verlag, 1999."},{"key":"57_CR11","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:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"57_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, LNCS 828 Springer-Verlag, 1994."},{"key":"57_CR13","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 garbage collector. Formal Aspects of Computing, 6:359\u2013390, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"57_CR14","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0020-0190(87)90135-9","volume":"24","author":"J. L. A. Snepscheut van de","year":"1987","unstructured":"J. L. A. van de Snepscheut. \u201cAlgorithms for on-the-fly garbage collection\u201d revisited. Information Processing Letters, 24:211\u2013216, 1987.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44612-5_57","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T09:35:57Z","timestamp":1550309757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44612-5_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679011","9783540446125"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-44612-5_57","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}