{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,11]],"date-time":"2026-09-11T04:31:48Z","timestamp":1789101108597,"version":"build-2803163510"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,6,10]],"date-time":"2007-06-10T00:00:00Z","timestamp":1181433600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,6,10]]},"DOI":"10.1145\/1250734.1250787","type":"proceedings-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T12:07:37Z","timestamp":1189771657000},"page":"456-467","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["CGCExplorer"],"prefix":"10.1145","author":[{"given":"Martin T.","family":"Vechev","sequence":"first","affiliation":[{"name":"Cambridge University, Cambridge, England UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[{"name":"IBM Research, Hawthorne, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David F.","family":"Bacon","sequence":"additional","affiliation":[{"name":"IBM Research, Hawthorne, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2007,6,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/872035.872080"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949328"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/579.587"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964020"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of International Computing Symposium","author":"Bowman H.","year":"1994","unstructured":"Bowman , H. , Derrick , J. , and Jones , RE . Modelling garbage collection algorithms . In Proceedings of International Computing Symposium ( 1994 ). Bowman, H., Derrick, J., and Jones, RE. Modelling garbage collection algorithms. In Proceedings of International Computing Symposium (1994)."},{"key":"e_1_3_2_1_6_1","volume-title":"the 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings","author":"Burdy L.","year":"2001","unstructured":"Burdy , L. B vs. Coq to prove a garbage collector . In the 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings ( 2001 ). Burdy, L. B vs. Coq to prove a garbage collector. In the 14th International Conference on Theorem Proving in Higher Order Logics: Supplemental Proceedings (2001)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96735"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/69622.357188"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/359642.359655"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/359897.359903"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359660"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040331"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/645611.662365"},{"key":"e_1_3_2_1_15_1","volume-title":"11th International Conference","author":"Jackson PB.","year":"1998","unstructured":"Jackson , PB. Verifying a garbage collection algorithm. In Theorem Proving in Higher Order Logics , 11th International Conference ( 1998 ). Jackson, PB. Verifying a garbage collection algorithm. In Theorem Proving in Higher Order Logics, 11th International Conference (1998)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover, vol828 of Lecture Notes in Computer Science","author":"Paulson L.","year":"1994","unstructured":"Paulson , L. Isabelle: A Generic Theorem Prover, vol828 of Lecture Notes in Computer Science . 1994 . Paulson, L. Isabelle: A Generic Theorem Prover, vol828 of Lecture Notes in Computer Science. 1994."},{"key":"e_1_3_2_1_18_1","volume-title":"Mathematical Foundations of Computer Science","author":"Prensa Nieto L.","year":"2000","unstructured":"Prensa Nieto , L. , and Esparza , J . Verifying single and multi-mutator garbage collectors with Owicki\/Gries in Isabelle\/HOL . In Mathematical Foundations of Computer Science ( 2000 ). Prensa Nieto, L., and Esparza, J. Verifying single and multi-mutator garbage collectors with Owicki\/Gries in Isabelle\/HOL. In Mathematical Foundations of Computer Science (2000)."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211305"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134022"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996846"}],"event":{"name":"PLDI '07: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"San Diego California USA","acronym":"PLDI '07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1250734.1250787","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1250734.1250787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:20Z","timestamp":1750243940000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1250734.1250787"}},"subtitle":["a semi-automated search procedure for provably correct concurrent collectors"],"short-title":[],"issued":{"date-parts":[[2007,6,10]]},"references-count":23,"alternative-id":["10.1145\/1250734.1250787","10.1145\/1250734"],"URL":"https:\/\/doi.org\/10.1145\/1250734.1250787","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1273442.1250787","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2007,6,10]]},"assertion":[{"value":"2007-06-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}