{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:53:12Z","timestamp":1726408392855},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030315139"},{"type":"electronic","value":"9783030315146"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-31514-6_6","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"73-103","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Refinement Proof for a Garbage Collector"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"6_CR1","unstructured":"PVS specification and verification system. \n                      http:\/\/pvs.csl.sri.com\n                      \n                    . Accessed 03 Mar 2019"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR3","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 TOPLAS 6, 333\u2013344 (1984)","journal-title":"ACM TOPLAS"},{"key":"6_CR4","unstructured":"Burdy, L.: B vs. Coq to prove a garbage collector. In: Boulton, R.J., Jackson, P.B. (eds.) 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings, pp. 85\u201397. September (2001)"},{"issue":"6","key":"6_CR5","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1093\/logcom\/13.6.815","volume":"13","author":"S Coupet-Grimal","year":"2003","unstructured":"Coupet-Grimal, S., Nouvet, C.: Formal verification of an incremental garbage collector. J. Logic Comput. 13(6), 815\u2013833 (2003)","journal-title":"J. Logic Comput."},{"issue":"11","key":"6_CR6","doi-asserted-by":"publisher","first-page":"966","DOI":"10.1145\/359642.359655","volume":"21","author":"EW Dijkstra","year":"1978","unstructured":"Dijkstra, E.W., Lamport, L., Martin, A., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection: an exercise in cooperation. ACM 21(11), 966\u2013975 (1978)","journal-title":"ACM"},{"key":"6_CR7","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":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-319-66107-0_28","volume-title":"Interactive Theorem Proving","author":"A Sandberg Ericsson","year":"2017","unstructured":"Sandberg Ericsson, A., Myreen, M.O., \u00c5man Pohjola, J.: A verified generational garbage collector for CakeML. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 444\u2013461. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66107-0_28"},{"issue":"6","key":"6_CR9","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/2813885.2738006","volume":"50","author":"Peter Gammie","year":"2015","unstructured":"Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-tso. In: ACM SIGPLAN Notices, vol. 50, pp. 99\u2013109. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-61474-5_103","volume-title":"Computer Aided Verification","author":"G Gonthier","year":"1996","unstructured":"Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 462\u2013465. Springer, Heidelberg (1996). \n                      https:\/\/doi.org\/10.1007\/3-540-61474-5_103"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1258","DOI":"10.1007\/BFb0098007","volume-title":"Parallel and Distributed Processing","author":"K Havelund","year":"1999","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: Rolim, J., et al. (eds.) IPPS 1999. LNCS, vol. 1586, pp. 1258\u20131283. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/BFb0098007"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME 1996: Industrial Benefit and Advances in Formal Methods","author":"K Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 662\u2013681. Springer, Heidelberg (1996). \n                      https:\/\/doi.org\/10.1007\/3-540-60973-3_113"},{"key":"6_CR13","unstructured":"Havelund, K., Shankar, N.: A mechanized refinement proof for a garbage collector. Technical report, October 1997. \n                      http:\/\/www.havelund.com\/Publications\/gc-refine-report.pdf"},{"key":"6_CR14","series-title":"Springer Series in Surface Sciences","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-319-21602-7","volume-title":"The Physics of Thin Film Optical Spectra","author":"O Stenzel","year":"2016","unstructured":"Stenzel, O.: The Physics of Thin Film Optical Spectra. SSSS, vol. 44, pp. 163\u2013180. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21602-7"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BFb0055139","volume-title":"Theorem Proving in Higher Order Logics","author":"PB Jackson","year":"1998","unstructured":"Jackson, P.B.: Verifying a garbage collection algorithm. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 225\u2013244. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0055139"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM TOPLAS 16(3), 872\u2013923 (1994)","journal-title":"ACM TOPLAS"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: ACM SIGPLAN Notices, vol. 42, pp. 468\u2013479. ACM (2007)","DOI":"10.1145\/1273442.1250788"},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF01788566","volume":"3","author":"C Pixley","year":"1988","unstructured":"Pixley, C.: An incremental garbage collection algorithm for multi-mutator systems. Distrib. Comput. 3, 41\u201350 (1988)","journal-title":"Distrib. Comput."},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF01211305","volume":"6","author":"DM Russinoff","year":"1994","unstructured":"Russinoff, D.M.: A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359\u2013390 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"6_CR20","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0020-0190(87)90135-9","volume":"24","author":"JLA Snepscheut van de","year":"1987","unstructured":"van de Snepscheut, J.L.A.: Algorithms for on-the-fly garbage collection revisited. Inf. Process. Lett. 24(4), 211\u2013216 (1987)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","From Reactive Systems to Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31514-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:26:51Z","timestamp":1569194811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31514-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030315139","9783030315146"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31514-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}