{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:28Z","timestamp":1773193528357,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_6","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T04:30:14Z","timestamp":1439872214000},"page":"84-99","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Validating Dominator Trees for a Fast, Verified Dominance Test"],"prefix":"10.1007","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"6_CR1","unstructured":"Allen, F.E., Cocke, J.: Graph theoretic constructs for program control flow analysis. Technical report, IBM T.J. Watson Research Center (1972)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2579080","volume":"36","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Demange, D., Pichardie, D.: Formal verification of an SSA-based middle-end for CompCert. ACM TOPLAS 36(1), 4:1\u20134:35 (2014)","journal-title":"ACM TOPLAS"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A verified compiler for an impure functional language. In: POPL 2010, pp. 93\u2013106. ACM (2010)","DOI":"10.1145\/1707801.1706312"},{"key":"6_CR4","unstructured":"Cooper, K.D., Harvey, T.J., Kennedy, K.: A simple, fast dominance algorithm. Technical report, Rice University (2006)"},{"issue":"4","key":"6_CR5","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM TOPLAS 13(4), 451\u2013490 (1991)","journal-title":"ACM TOPLAS"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-75560-9_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Z Dargaye","year":"2007","unstructured":"Dargaye, Z., Leroy, X.: Mechanized verification of CPS transformations. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 211\u2013225. Springer, Heidelberg (2007)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-46663-6_12","volume-title":"Compiler Construction","author":"D Demange","year":"2015","unstructured":"Demange, D., Pichardie, D., Stefanesco, L.: Verifying fast and sparse SSA-based optimizations in Coq. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 233\u2013252. Springer, Heidelberg (2015)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Fluet, M., Weeks, S.: Contification using dominators. In: Proceedings of ICFP 2001, pp. 2\u201313. ACM (2001)","DOI":"10.1145\/507669.507639"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-642-38527-8_26","volume-title":"Experimental Algorithms","author":"L Georgiadis","year":"2013","unstructured":"Georgiadis, L., Laura, L., Parotsidis, N., Tarjan, R.E.: Dominator certification and independent spanning trees: an experimental study. In: Demetrescu, C., Marchetti-Spaccamela, A., Bonifaci, V. (eds.) SEA 2013. LNCS, vol. 7933, pp. 284\u2013295. Springer, Heidelberg (2013)"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.7155\/jgaa.00119","volume":"10","author":"L Georgiadis","year":"2006","unstructured":"Georgiadis, L., Tarjan, R.E., Werneck, R.F.: Finding dominators in practice. J. Graph Algorithms Appl. 10(1), 69\u201394 (2006)","journal-title":"J. Graph Algorithms Appl."},{"key":"6_CR11","unstructured":"Georgiadis, L., Tarjan, R.E.: Dominator tree verification and vertex-disjoint paths. In: Proceedings of SODA 2005, pp. 433\u2013442. ACM (2005)"},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T Lengauer","year":"1979","unstructured":"Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM TOPLAS 1(1), 121\u2013141 (1979)","journal-title":"ACM TOPLAS"},{"issue":"7","key":"6_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4","key":"6_CR14","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. JAR 43(4), 363\u2013446 (2009)","journal-title":"JAR"},{"key":"6_CR15","unstructured":"Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Workshop on ML, pp. 77\u201386 (1998)"},{"key":"6_CR16","unstructured":"Parotsidis, N., Georgiadis, L.: 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), vol. 1, pp. 15\u201320. Epoka University (2013)"},{"key":"6_CR17","volume-title":"Introduction to Algorithms","author":"RL Rivest","year":"2009","unstructured":"Rivest, R.L., Cormen, T.H., Leiserson, C.E., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013, pp. 175\u2013186. ACM (2013)","DOI":"10.1145\/2499370.2462164"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-35308-6_6","volume-title":"Certified Programs and Proofs","author":"J Zhao","year":"2012","unstructured":"Zhao, J., Zdancewic, S.: Mechanized verification of computing dominators for formalizing compilers. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 27\u201342. Springer, Heidelberg (2012)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Zhao, J., Zdancewic, S., Nagarakatte, S., Martin, M.: Formalizing the LLVM intermediate representation for verified program transformation. In: POPL 2012, pp. 427\u2013440. ACM (2012)","DOI":"10.1145\/2103621.2103709"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T13:14:31Z","timestamp":1559222071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}