{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:32Z","timestamp":1772163992057,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":50,"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.1250737","type":"proceedings-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T12:07:37Z","timestamp":1189771657000},"page":"12-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":139,"title":["CheckFence"],"prefix":"10.1145","author":[{"given":"Sebastian","family":"Burckhardt","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]},{"given":"Milo M. K.","family":"Martin","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]}],"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\/1119479.1119480"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065042"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_45"},{"key":"e_1_3_2_1_5_1","first-page":"168","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2988","author":"Clarke E.","year":"2004","unstructured":"E. Clarke , D. Kroening , and F. Lerda . A tool for checking ANSI-C programs . In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2988 , pages 168 -- 176 . Springer , 2004 . E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2988, pages 168--176. Springer, 2004."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_44"},{"key":"e_1_3_2_1_7_1","volume-title":"Alpha Architecture Reference Manual","author":"Compaq Computer Corporation","year":"2002","unstructured":"Compaq Computer Corporation . Alpha Architecture Reference Manual , 4 th edition, January 2002 . Compaq Computer Corporation. Alpha Architecture Reference Manual, 4th edition, January 2002.","edition":"4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645957.758425"},{"key":"e_1_3_2_1_9_1","first-page":"38","volume-title":"Symposium on Research on Integrated Systems","author":"Dill D.","year":"1993","unstructured":"D. Dill , S. Park , and A. Nowatzyk . Formal specification of abstract memory models . In Symposium on Research on Integrated Systems , pages 38 -- 52 . MIT Press , 1993 . D. Dill, S. Park, and A. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems, pages 38--52. MIT Press, 1993."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007945"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/782814.782854"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_3_2_1_13_1","volume-title":"PowerPC Architecture Book v2.02","author":"Frey B.","year":"2005","unstructured":"B. Frey . PowerPC Architecture Book v2.02 . International Business Machines Corporation , 2005 . B. Frey. PowerPC Architecture Book v2.02. International Business Machines Corporation, 2005."},{"key":"e_1_3_2_1_14_1","first-page":"44","volume-title":"Computer--Aided Verification (CAV), LNCS 3114","author":"Gao H.","year":"2004","unstructured":"H. Gao and W. Hesslink . A formal reduction for lock-free parallel algorithms . In Computer--Aided Verification (CAV), LNCS 3114 , pages 44 -- 56 . Springer , 2004 . H. Gao and W. Hesslink. A formal reduction for lock-free parallel algorithms. In Computer--Aided Verification (CAV), LNCS 3114, pages 44--56. Springer, 2004."},{"key":"e_1_3_2_1_15_1","first-page":"401","volume-title":"Computer-Aided Verification (CAV), LNCS 3114","author":"Gopalakrishnan G.","year":"2004","unstructured":"G. Gopalakrishnan , Y. Yang , and H. Sivaraj . QB or not QB: An efficient execution verification tool for memory orderings . In Computer-Aided Verification (CAV), LNCS 3114 , pages 401 -- 413 , 2004 . G. Gopalakrishnan, Y. Yang, and H. Sivaraj. QB or not QB: An efficient execution verification tool for memory orderings. In Computer-Aided Verification (CAV), LNCS 3114, pages 401--413, 2004."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/645959.676137"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11795490_3"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_3_2_1_20_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer's Manual","author":"Intel Corporation","unstructured":"Intel Corporation . Intel 64 and IA-32 Architectures Software Developer's Manual , Volume 3A, November 2006 . Intel Corporation. Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 3A, November 2006."},{"key":"e_1_3_2_1_21_1","volume-title":"Book 2, rev. 2.2","author":"Intel Corporation","year":"2006","unstructured":"Intel Corporation . Intel Itanium Architecture Software Developer's Manual , Book 2, rev. 2.2 , January 2006 . Intel Corporation. Intel Itanium Architecture Software Developer's Manual, Book 2, rev. 2.2, January 2006."},{"key":"e_1_3_2_1_22_1","volume-title":"September","author":"Intel Corporation","year":"2006","unstructured":"Intel Corporation . Intel Threading Building Blocks , September 2006 . Intel Corporation. Intel Threading Building Blocks, September 2006."},{"key":"e_1_3_2_1_23_1","volume-title":"Architecture Principles of Operation","author":"International Business Machines Corporation","year":"2000","unstructured":"International Business Machines Corporation . Architecture Principles of Operation , first edition, December 2000 . International Business Machines Corporation. Architecture Principles of Operation, first edition, December 2000."},{"key":"e_1_3_2_1_24_1","first-page":"66","volume-title":"TV'06 Workshop, Federated Logic Conference (FLoC)","author":"Jacobs B.","year":"2006","unstructured":"B. Jacobs , J. Smans , F. Piessens , and W. Schulte . A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs . In TV'06 Workshop, Federated Logic Conference (FLoC) , pages 66 -- 77 , 2006 . B. Jacobs, J. Smans, F. Piessens, and W. Schulte. A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. In TV'06 Workshop, Federated Logic Conference (FLoC), pages 66--77, 2006."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_11"},{"key":"e_1_3_2_1_27_1","volume-title":"PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP)","author":"Lea D.","year":"2004","unstructured":"D. Lea . The java.util. concurrent synchronizer framework . In PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP) , 2004 . D. Lea. The java.util.concurrent synchronizer framework. In PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP), 2004."},{"key":"e_1_3_2_1_28_1","volume-title":"October","author":"Luchangco V.","year":"2006","unstructured":"V. Luchangco . Personal communications , October 2006 . V. Luchangco. Personal communications, October 2006."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/563998.564039"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996848"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/259380.259442"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/215399.215413"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134019"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_9"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2004.12.005"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095408.1095421"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1898953.1898968"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2006.16"},{"key":"e_1_3_2_1_48_1","volume-title":"The SPARC Architecture Manual Version 9","author":"Weaver D.","year":"1994","unstructured":"D. Weaver and T. Germond , editors . The SPARC Architecture Manual Version 9 . PTR Prentice Hall , 1994 . D. Weaver and T. Germond, editors. The SPARC Architecture Manual Version 9. PTR Prentice Hall, 1994."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065013"},{"key":"e_1_3_2_1_50_1","volume-title":"Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci., 89(3)","author":"Yahav E.","year":"2003","unstructured":"E. Yahav and M. Sagiv . Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci., 89(3) , 2003 . E. Yahav and M. Sagiv. Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci., 89(3), 2003."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"}],"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.1250737","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1250734.1250737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:19Z","timestamp":1750243939000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1250734.1250737"}},"subtitle":["checking consistency of concurrent data types on relaxed memory models"],"short-title":[],"issued":{"date-parts":[[2007,6,10]]},"references-count":50,"alternative-id":["10.1145\/1250734.1250737","10.1145\/1250734"],"URL":"https:\/\/doi.org\/10.1145\/1250734.1250737","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1273442.1250737","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"}}]}}