{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:48Z","timestamp":1759638948111,"version":"3.37.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893624"},{"type":"electronic","value":"9783319893631"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89363-1_12","type":"book-chapter","created":{"date-parts":[[2018,4,3]],"date-time":"2018-04-03T09:04:43Z","timestamp":1522746283000},"page":"207-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Fast Computation of Arbitrary Control Dependencies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0420-2745","authenticated-orcid":false,"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,4]]},"reference":[{"key":"12_CR1","unstructured":"Why3, a tool for deductive program verification, GNU LGPL 2.1, development version, January 2018. http:\/\/why3.lri.fr"},{"issue":"2","key":"12_CR2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.ipl.2007.10.002","volume":"106","author":"T Amtoft","year":"2008","unstructured":"Amtoft, T.: Slicing for modern program structures: a theory for eliminating irrelevant loops. Inf. Process. Lett. 106(2), 45\u201351 (2008)","journal-title":"Inf. Process. Lett."},{"key":"12_CR3","unstructured":"Amtoft, T., Androutsopoulos, K., Clark, D.: Correctness of slicing finite state machines. Technical report RN\/13\/22. University College London, December 2013"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-662-49630-5_11","volume-title":"Foundations of Software Science and Computation Structures","author":"T Amtoft","year":"2016","unstructured":"Amtoft, T., Banerjee, A.: A theory of slicing for probabilistic control flow graphs. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 180\u2013196. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_11"},{"key":"12_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bilardi, G., Pingali, K.: Generalized dominance and control dependence. In: PLDI, pp. 291\u2013300. ACM (1996)","DOI":"10.1145\/249069.231435"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Blazy, S., Maroneze, A., Pichardie, D.: Verified validation of program slicing. In: CPP 2015, pp. 109\u2013117 (2015)","DOI":"10.1145\/2676724.2693169"},{"issue":"4","key":"12_CR8","doi-asserted-by":"crossref","first-page":"1533","DOI":"10.1137\/070693217","volume":"38","author":"AL Buchsbaum","year":"2008","unstructured":"Buchsbaum, A.L., Georgiadis, L., Kaplan, H., Rogers, A., Tarjan, R.E., Westbrook, J.: Linear-time algorithms for dominators and other path-evaluation problems. SIAM J. Comput. 38(4), 1533\u20131573 (2008)","journal-title":"SIAM J. Comput."},{"key":"12_CR9","unstructured":"Conchon, S., Filli\u00e2tre, J., Signoles, J.: Designing a generic graph library using ML functors. In: Moraz\u00e1n, M.T. (ed.) Trends in Functional Programming, vol. 8, pp. 124\u2013140. Intellect, Bristol (2007)"},{"issue":"1\u201310","key":"12_CR10","first-page":"1","volume":"4","author":"KD Cooper","year":"2001","unstructured":"Cooper, K.D., Harvey, T.J., Kennedy, K.: A simple, fast dominance algorithm. Softw. Pract. Exp. 4(1\u201310), 1\u20138 (2001)","journal-title":"Softw. Pract. Exp."},{"issue":"49","key":"12_CR11","doi-asserted-by":"crossref","first-page":"6809","DOI":"10.1016\/j.tcs.2011.08.033","volume":"412","author":"S Danicic","year":"2011","unstructured":"Danicic, S., Barraclough, R.W., Harman, M., Howroyd, J., Kiss, \u00c1., Laurence, M.R.: A unifying theory of control dependence and its application to arbitrary program structures. Theor. Comput. Sci. 412(49), 6809\u20136842 (2011)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"12_CR12","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"issue":"3","key":"12_CR13","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Georgiadis, L., Tarjan, R.E.: Dominator tree certification and divergent spanning trees. ACM Trans. Algorithms 12(1), 11:1\u201311:42 (2016)","DOI":"10.1145\/2764913"},{"issue":"1","key":"12_CR16","doi-asserted-by":"crossref","first-page":"69","DOI":"10.7155\/jgaa.00119","volume":"10","author":"L Georgiadis","year":"2006","unstructured":"Georgiadis, L., Tarjan, R.E., Werneck, R.F.F.: Finding dominators in practice. J. Graph Algorithms Appl. 10(1), 69\u201394 (2006)","journal-title":"J. Graph Algorithms Appl."},{"key":"12_CR17","unstructured":"L\u00e9chenet, J.-C.: Formalization of weak control dependence (2018). http:\/\/perso.ecp.fr\/~lechenetjc\/control\/"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-662-49665-7_11","volume-title":"Fundamental Approaches to Software Engineering","author":"J-C L\u00e9chenet","year":"2016","unstructured":"L\u00e9chenet, J.-C., Kosmatov, N., Le Gall, P.: Cut branches before looking for bugs: sound verification on relaxed slices. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 179\u2013196. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_11"},{"issue":"1","key":"12_CR19","doi-asserted-by":"crossref","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. 1(1), 121\u2013141 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"12_CR20","doi-asserted-by":"crossref","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"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Ottenstein, K.J., Ottenstein, L.M.: The program dependence graph in a software development environment. In: The First ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (SDE 1984), pp. 177\u2013184. ACM Press (1984)","DOI":"10.1145\/800020.808263"},{"issue":"9","key":"12_CR22","doi-asserted-by":"crossref","first-page":"965","DOI":"10.1109\/32.58784","volume":"16","author":"A Podgurski","year":"1990","unstructured":"Podgurski, A., Clarke, L.A.: A formal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Trans. Softw. Eng. 16(9), 965\u2013979 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29(5) (2007). Article No. 27","DOI":"10.1145\/1275497.1275502"},{"key":"12_CR24","unstructured":"The Coq Development Team: The Coq proof assistant, v8.6 (2017). http:\/\/coq.inria.fr\/"},{"issue":"3","key":"12_CR25","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3), 121\u2013189 (1995)","journal-title":"J. Prog. Lang."},{"key":"12_CR26","unstructured":"Wasserrab, D.: From formal semantics to verified slicing: a modular framework with applications in language based security. Ph.D. thesis, Karlsruhe Inst. of Techn. (2011)"},{"key":"12_CR27","unstructured":"Weiser, M.: Program slicing. In: ICSE 1981 (1981)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89363-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,13]],"date-time":"2019-10-13T20:17:06Z","timestamp":1570997826000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89363-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893624","9783319893631"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89363-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}