{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:13:21Z","timestamp":1775672001762,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779107","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"143-156","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanized Dominator Tree Certification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0420-2745","authenticated-orcid":false,"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"first","affiliation":[{"name":"Universit\u00e9 C\u00f4te d'Azur, Inria, Sophia Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Allen and John Cocke","author":"Frances","year":"1972","unstructured":"Frances E. Allen and John Cocke. 1972. Graph-theoretic constructs for program control flow analysis. IBM T.J. Watson Research Center."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-022-09655-X"},{"key":"e_1_3_2_1_3_1","volume-title":"Appel and Jens Palsberg","author":"Andrew","year":"2002","unstructured":"Andrew W. Appel and Jens Palsberg. 2002. Modern Compiler Implementation in Java, 2nd edition. Cambridge University Press. isbn:0-521-82060-X","edition":"2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/070693217"},{"key":"e_1_3_2_1_7_1","volume-title":"Fast Dominance Algorithm","author":"Cooper Keith D.","unstructured":"Keith D. Cooper, Timothy J. Harvey, and Ken Kennedy. 2006. A Simple, Fast Dominance Algorithm. Rice University."},{"key":"e_1_3_2_1_8_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press. isbn:978-0-262-03384-8 http:\/\/mitpress.mit.edu\/books\/introduction-algorithms","edition":"3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JDA.2013.10.003"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38527-8_26"},{"key":"e_1_3_2_1_12_1","volume-title":"2nd International Symposium on Computing in Informatics and Mathematics (ISCIM","author":"Georgiadis Loukas","year":"2013","unstructured":"Loukas Georgiadis and Nikos Parotsidis. 2013. Dominators in Directed Graphs: A Survey of Recent Results, Applications, and Open Problems. In 2nd International Symposium on Computing in Informatics and Mathematics (ISCIM 2013). 15\u201320."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2928271"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2764913"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.7155\/JGAA.00119"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575681"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_19"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357071"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-009-9155-4"},{"key":"e_1_3_2_1_20_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems. SEE. http:\/\/xavierleroy.org\/publi\/erts2016_compcert.pdf","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE. http:\/\/xavierleroy.org\/publi\/erts2016_compcert.pdf"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17795214"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_6"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:41Z","timestamp":1775667281000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":23,"alternative-id":["10.1145\/3779031.3779107","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779107","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}