{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:18:22Z","timestamp":1742984302659,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031666759"},{"type":"electronic","value":"9783031666766"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66676-6_10","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"195-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["What Is a\u00a0Garbage Collector? An\u00a0Exercise in\u00a0Compositional Refinement"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Third Annual Symposium on Logic in Computer Science, pp. 165\u2013175. IEEE. Computer Society Press, July 1988","DOI":"10.1109\/LICS.1988.5115"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"RJR Back","year":"1987","unstructured":"Back, R.J.R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49\u201368 (1987)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Back, R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998)","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Back, R.-J.R.,\u00a0Kurki-Suonio, F.: Distributed cooperation with action systems. ACM Trans. Programm. Lang. Syst. (TOPLAS) 10(4), 513\u2013554 (1988)","DOI":"10.1145\/48022.48023"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Back, R.J.R.: Refinement calculus, Part\u00a0II: Parallel and reactive programs. In: de\u00a0Bakker et\u00a0al. [12], pp. 67\u201393","DOI":"10.1007\/3-540-52559-9_61"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Back, R.J.R., von Wright, J.: Refinement calculus, Part\u00a0I: Sequential nondeterministic programs. In: de\u00a0Bakker et\u00a0al. [12], pp. 42\u201366","DOI":"10.1007\/3-540-52559-9_60"},{"issue":"3","key":"10_CR8","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/579.587","volume":"6","author":"M Ben-Ari","year":"1984","unstructured":"Ben-Ari, M.: Algorithms for on-the-fly garbage collection. ACM Trans. Programm. Lang. Syst. (TOPLAS) 6(3), 333\u2013344 (1984)","journal-title":"ACM Trans. Programm. Lang. Syst. (TOPLAS)"},{"key":"10_CR9","volume-title":"A Computational Logic Handbook","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)"},{"key":"10_CR10","unstructured":"Lilian Burdy. B vs. Coq to prove a garbage collector. In: The 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings (2001)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Mani Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"de\u00a0Bakker, J.W., de\u00a0Roever, W.-P., Rozenberg, G. (eds.) Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, vol. 430. LNCS. Springer (1990)","DOI":"10.1007\/3-540-52559-9"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"de\u00a0Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparrison. Number\u00a047 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Presss (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21(11), 966\u2013975 (1978)","DOI":"10.1145\/359642.359655"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 70\u201383. ACM (1994)","DOI":"10.1145\/174675.174673"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-tso. In: ACM SIGPLAN Notices, vol.\u00a050, pp. 99\u2013109. ACM (2015)","DOI":"10.1145\/2813885.2738006"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: International Conference on Computer Aided Verification, pp. 462\u2013465. Springer (1996)","DOI":"10.1007\/3-540-61474-5_103"},{"issue":"12","key":"10_CR18","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1145\/359897.359903","volume":"20","author":"D Gries","year":"1977","unstructured":"Gries, D.: An exercise in proving parallel programs correct. Commun. ACM 20(12), 921\u2013930 (1977)","journal-title":"Commun. ACM"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: Rolim, J., et\u00a0al. (ed.) Parallel and Distributed Processing, vol. 1586. LNCS, pp. 1258\u20131283. Springer (1999)","DOI":"10.1007\/BFb0098007"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Havelund, K., Shankar, N.: A refinement proof for a garbage collector. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds.) From Reactive Systems to Cyber-Physical Systems - Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday, vol. 11500, pp. 73\u2013103. Springer (2019)","DOI":"10.1007\/978-3-030-31514-6_6"},{"issue":"10","key":"10_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576\u2013583 (1969)","journal-title":"Comm. ACM"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Jackson, P.B.: Verifying a garbage collection algorithm. In: International Conference on Theorem Proving in Higher Order Logics, pp. 225\u2013244. Springer (1998)","DOI":"10.1007\/BFb0055139"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596\u2013619 (1983)","journal-title":"ACM TOPLAS"},{"key":"10_CR24","unstructured":"Jones, C.B.: Systematic software development using VDM. In: Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition (1990)"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Jones, C.B., Yatapanage, N.: Investigating the limits of rely\/guarantee relations based on a concurrent garbage collector example. Formal Aspects Comput. 31, 353\u2013374 (2019)","DOI":"10.1007\/s00165-019-00482-3"},{"key":"10_CR26","unstructured":"Lamport, L.: The temporal logic of actions. Technical Report\u00a079, Digital Systems Research Center, 130 Lytton Avenue; Palo Alto, California 94301, December 1991"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems\u2014Specification, vol.\u00a01. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"10_CR28","unstructured":"McCarthy, J., Abrahams, P.W., Edwards, D.J., Hart, T.P., Levin, M.I.: LISP 1.5 Programmer\u2019s Manual. The MIT Press, Cambridge, MA (1965)"},{"key":"10_CR29","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall (1990)"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Prensa Nieto, L.: Esparza, J.: Verifying single and multi-mutator garbage collectors with Owicki-Gries in Isabelle\/HOL. In: International Symposium on Mathematical Foundations of Computer Science, pp. 619\u2013628. Springer (2000)","DOI":"10.1007\/3-540-44612-5_57"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer (2002). Isabelle home page: http:\/\/isabelle.in.tum.de\/","DOI":"10.1007\/3-540-45949-9"},{"key":"10_CR32","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107\u2013125, February 1995. PVS home page: http:\/\/pvs.csl.sri.com","DOI":"10.1109\/32.345827"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Pavlovic, D., Pepper, P., Smith, D.R.: Formal derivation of concurrent garbage collectors. In: International Conference on Mathematics of Program Construction, pp. 353\u2013376. Springer (2010)","DOI":"10.1007\/978-3-642-13321-3_20"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Ann. IEEE Symp. on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M.: A mechanically verified incremental garbage collector. Formal Aspects Comput. 6(4), 359\u2013390 (1994)","DOI":"10.1007\/BF01211305"},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality: The Significant Difference (Revised lectures from International Symposium COMPOS\u201997)","author":"N Shankar","year":"1997","unstructured":"Shankar, N.: Lazy compositional verification. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) Compositionality: The Significant Difference (Revised lectures from International Symposium COMPOS\u201997). Lecture Notes in Computer Science, vol. 1536. Springer, Bad Malente, Germany (1997)"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Van de Snepscheut, J.L.A.: \u201cAlgorithms for on-the-fly garbage collection\u201d revisited. Inf. Process. Lett. 24(4), 211\u2013216 (1987)","DOI":"10.1016\/0020-0190(87)90135-9"}],"container-title":["Lecture Notes in Computer Science","The Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66676-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T19:15:09Z","timestamp":1732734909000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66676-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666759","9783031666766"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66676-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}