{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:04Z","timestamp":1770896164306,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642353079","type":"print"},{"value":"9783642353086","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_6","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"27-42","source":"Crossref","is-referenced-by-count":10,"title":["Mechanized Verification of Computing Dominators for Formalizing Compilers"],"prefix":"10.1007","author":[{"given":"Jianzhou","family":"Zhao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","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)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Modern Compiler Implementation in C: Basic Techniques. Cambridge University Press (1997)","DOI":"10.1017\/CBO9781139174930"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-28869-2_3","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2012","unstructured":"Barthe, G., Demange, D., Pichardie, D.: A Formally Verified SSA-Based Middle-End. In: Seidl, H. (ed.)ESOP 2012. LNCS, vol.\u00a07211, pp. 47\u201366. Springer, Heidelberg (2012)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"6_CR5","unstructured":"Cooper, K.D., Harvey, T.J., Kennedy, K.: A simple, fast dominance algorithm (2000), \n                  \n                    www.cs.rice.edu\/~keith\/Embed\/dom.pdf"},{"key":"6_CR6","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 Trans. Program. Lang. Syst.\u00a013, 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR7","unstructured":"Georgiadis, L., Tarjan, R.E.: Dominator tree verification and vertex-disjoint paths. In: SODA 2005, pp. 433\u2013442 (2005)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-540-30140-0_60","volume-title":"Algorithms \u2013 ESA 2004","author":"L. Georgiadis","year":"2004","unstructured":"Georgiadis, L., Werneck, R.F., Tarjan, R.E., August, D.I.: Finding Dominators in Practice. In: Albers, S., Radzik, T. (eds.) ESA 2004. LNCS, vol.\u00a03221, pp. 677\u2013688. Springer, Heidelberg (2004)"},{"issue":"1","key":"6_CR9","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321921.321938","volume":"23","author":"J.B. Kam","year":"1976","unstructured":"Kam, J.B., Ullman, J.D.: Global data flow analysis and iterative algorithms. J. ACM\u00a023(1), 158\u2013171 (1976)","journal-title":"J. ACM"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"6_CR11","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 Trans. Program. Lang. Syst.\u00a01, 121\u2013141 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"6_CR12","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. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"6_CR13","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/570886.570887","volume":"24","author":"G. Ramalingam","year":"2002","unstructured":"Ramalingam, G.: On loops, dominators, and dominance frontiers. ACM Trans. Program. Lang. Syst.\u00a024(5), 455\u2013490 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL 2012 (2012)","DOI":"10.1145\/2103656.2103709"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:13:50Z","timestamp":1620134030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}