{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:00:41Z","timestamp":1743022841691,"version":"3.40.3"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452360"},{"type":"electronic","value":"9783030452377"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Change impact analysis techniques determine the components affected by a change to a software system, and are used as part of many program analysis techniques and tools, e.g., in regression test selection, build systems, and compilers. The correctness of such analyses usually depends both on domain-specific properties and change impact analysis, and is rarely established formally, which is detrimental to trustworthiness. We present a formalization of change impact analysis with machine-checked proofs of correctness in the Coq proof assistant. Our formal model factors out domain-specific concerns and captures system components and their interrelations in terms of dependency graphs. Using compositionality, we also capture hierarchical impact analysis formally for the first time, which, e.g., can capture when impacted files are used to locate impacted tests inside those files. We refined our verified impact analysis for performance, extracted it to efficient executable OCaml code, and integrated it with a regression test selection tool, one regression proof selection tool, and one build system, replacing their existing impact analyses. We then evaluated the resulting toolchains on several open source projects, and our results show that the toolchains run with only small differences compared to the original running time. We believe our formalization can provide a basis for formally proving domain-specific techniques using change impact analysis correct, and our verified code can be integrated with additional tools to increase their reliability.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_9","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"137-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Practical Machine-Checked Formalization of Change Impact Analysis"],"prefix":"10.1007","author":[{"given":"Karl","family":"Palmskog","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmet","family":"Celik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milos","family":"Gligoric","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Acharya, M., Robinson, B.: Practical change impact analysis based on static program slicing for industrial software systems. In: International Conference on Software Engineering. pp. 746\u2013755. ACM, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1985793.1985898","DOI":"10.1145\/1985793.1985898"},{"key":"9_CR2","unstructured":"Appel, A.W.: Efficient verified red-black trees (2011), https:\/\/www.cs.princeton.edu\/~appel\/papers\/redblack.pdf, last accessed 21 Feb 2020"},{"key":"9_CR3","unstructured":"Arnold, R.S.: Software Change Impact Analysis. IEEE Computer Society, Los Alamitos, CA, USA (1996)"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Arnold, R.S., Bohner, S.A.: Impact analysis - towards a framework for comparison. In: International Conference on Software Maintenance. pp. 292\u2013301. IEEE Computer Society, Washington, DC, USA (1993). https:\/\/doi.org\/10.1109\/ICSM.1993.366933","DOI":"10.1109\/ICSM.1993.366933"},{"key":"9_CR5","unstructured":"Bazel team: Bazel Blog, https:\/\/blog.bazel.build, last accessed 20 Feb 2020"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: the calculus of inductive constructions. Springer, Heidelberg, Germany (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Gonthier, G., Ould\u00a0Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) International Conference on Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg, Germany (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_11","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. In: SIGCOMM Conference. pp. 265\u2013276. ACM, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1080091.1080123","DOI":"10.1145\/1080091.1080123"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg, Germany (1997). https:\/\/doi.org\/10.1007\/BFb0014565","DOI":"10.1007\/BFb0014565"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Cai, H., Santelices, R.: A comprehensive study of the predictive accuracy of dynamic change-impact analysis. J. Syst. Softw. 103(C), 248\u2013265 (2015). https:\/\/doi.org\/10.1016\/j.jss.2015.02.018","DOI":"10.1016\/j.jss.2015.02.018"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Celik, A., Palmskog, K., Gligoric, M.: iCoq: Regression proof selection for large-scale verification projects. In: International Conference on Automated Software Engineering. pp. 171\u2013182. IEEE Computer Society, Washington, DC, USA (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115630","DOI":"10.1109\/ASE.2017.8115630"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Celik, A., Palmskog, K., Gligoric, M.: A regression proof selection tool for Coq. In: International Conference on Software Engineering, Tool Demonstrations. pp. 117\u2013120. ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3183440.3183493","DOI":"10.1145\/3183440.3183493"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Chen, R., Cohen, C., L\u00e9vy, J.J., Merz, S., Th\u00e9ry, L.: Formal Proofs of Tarjan\u2019s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) International Conference on Interactive Theorem Proving. pp. 13:1\u201313:19. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.13","DOI":"10.4230\/LIPIcs.ITP.2019.13"},{"key":"9_CR14","unstructured":"Chodorow, K.: Trimming the (build) tree with Bazel, https:\/\/www.kchodorow.com\/blog\/2015\/07\/23\/trimming-the-build-tree-with-bazel\/, last accessed 20 Feb 2020"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Christakis, M., Leino, K.R.M., Schulte, W.: Formalizing and verifying a modern build language. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) Symposium on Formal Methods. LNCS, vol.\u00a08442, pp. 643\u2013657. Springer, Cham, Switzerland (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_43","DOI":"10.1007\/978-3-319-06410-9_43"},{"key":"9_CR16","unstructured":"Cohen, C., Th\u00e9ry, L.: Formalization of Tarjan 72 algorithm in Coq with Mathematical Components and SSReflect, https:\/\/github.com\/CohenCyril\/tarjan, last accessed 21 Feb 2020"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Coquand, T., Paulin-Mohrin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) International Conference on Computer Logic. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg, Germany (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_47","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electronic Notes in Theoretical Computer Science 151(1), 75\u201391 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.11.024","DOI":"10.1016\/j.entcs.2005.11.024"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Delaware, B., Suriyakarn, S., Pit-Claudel, C., Ye, Q., Chlipala, A.: Narcissus: Correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3(ICFP) (2019). https:\/\/doi.org\/10.1145\/3341686","DOI":"10.1145\/3341686"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Esfahani, H., Fietz, J., Ke, Q., Kolomiets, A., Lan, E., Mavrinac, E., Schulte, W., Sanches, N., Kandula, S.: CloudBuild: Microsoft\u2019s distributed and caching build service. In: International Conference on Software Engineering, Software Engineering in Practice. pp. 11\u201320. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2889160.2889222","DOI":"10.1145\/2889160.2889222"},{"key":"9_CR22","unstructured":"ExtLib team: OCaml Extended standard Library, https:\/\/github.com\/ygrek\/ocaml-extlib, last accessed 20 Feb 2020"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) European Symposium on Programming. LNCS, vol.\u00a02986, pp. 370\u2013384. Springer, Heidelberg, Germany (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_26","DOI":"10.1007\/978-3-540-24725-8_26"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Fonseca, P., Zhang, K., Wang, X., Krishnamurthy, A.: An empirical study on the correctness of formally verified distributed systems. In: European Conference on Computer Systems. pp. 328\u2013343. ACM, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3064176.3064183","DOI":"10.1145\/3064176.3064183"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) International Conference on Theorem Proving in Higher Order Logics. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg, Germany (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Gligoric, M., Eloussi, L., Marinov, D.: Practical regression test selection with dynamic file dependencies. In: International Symposium on Software Testing and Analysis. pp. 211\u2013222. ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2771783.2771784","DOI":"10.1145\/2771783.2771784"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Gligoric, M., Schulte, W., Prasad, C., van Velzen, D., Narasamdya, I., Livshits, B.: Automated migration of build scripts using dynamic analysis and search-based refactoring. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications. pp. 599\u2013616. ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2714064.2660239","DOI":"10.1145\/2714064.2660239"},{"key":"9_CR28","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Notices of the American Mathematical Society 55(11), 1382\u20131393 (2008), http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le\u00a0Roux, S., Mahboubi, A., O\u2019Connor, R., Ould\u00a0Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) International Conference on Interactive Theorem Proving. LNCS, vol.\u00a07998, pp. 163\u2013179. Springer, Heidelberg, Germany (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3(2), 95\u2013152 (2010). https:\/\/doi.org\/10.6092\/issn.1972-5787\/1979","DOI":"10.6092\/issn.1972-5787\/1979"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: International Conference on Functional Programming. pp. 163\u2013175. ACM, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/2034773.2034798","DOI":"10.1145\/2034773.2034798"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Jourdan, J.H., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) International Conference on Interactive Theorem Proving. pp. 18:1\u201318:20. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.18","DOI":"10.4230\/LIPIcs.ITP.2019.18"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Kell, S., Mulligan, D.P., Sewell, P.: The missing link: Explaining ELF static linking, semantically. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications. pp. 607\u2013623. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2983990.2983996","DOI":"10.1145\/2983990.2983996"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: Opportunities, applications, and challenges. In: Workshop on Future of Software Engineering Research. pp. 201\u2013204. ACM, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1882362.1882405","DOI":"10.1145\/1882362.1882405"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: Conference on Certified Programs and Proofs. pp. 137\u2013146. ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676724.2693165","DOI":"10.1145\/2676724.2693165"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Law, J., Rothermel, G.: Whole program path-based dynamic impact analysis. In: International Conference on Software Engineering. pp. 308\u2013318. IEEE Computer Society, Washington, DC, USA (2003). https:\/\/doi.org\/10.1109\/ICSE.2003.1201210","DOI":"10.1109\/ICSE.2003.1201210"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Legunsen, O., Hariri, F., Shi, A., Lu, Y., Zhang, L., Marinov, D.: An extensive study of static regression test selection in modern software evolution. In: International Symposium on Foundations of Software Engineering. pp. 583\u2013594. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2950290.2950361","DOI":"10.1145\/2950290.2950361"},{"key":"9_CR38","unstructured":"Lehnert, S.: A review of software change impact analysis. Tech. rep., Technische Universit\u00e4t Ilmenau, Ilmenau, Germany (2011), https:\/\/nbn-resolving.org\/urn:nbn:de:gbv:ilm1-2011200618"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg, Germany (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12","DOI":"10.1007\/3-540-39185-1_12"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Luo, Q., Hariri, F., Eloussi, L., Marinov, D.: An empirical analysis of flaky tests. In: International Symposium on Foundations of Software Engineering. pp. 643\u2013653. ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2635868.2635920","DOI":"10.1145\/2635868.2635920"},{"key":"9_CR42","unstructured":"MathComp team: Mathematical Components project, https:\/\/math-comp.github.io, last accessed 20 Feb 2020"},{"key":"9_CR43","doi-asserted-by":"publisher","unstructured":"Mitchell, N.: Shake before building: Replacing Make with Haskell. In: International Conference on Functional Programming. pp. 55\u201366. ACM, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2364527.2364538","DOI":"10.1145\/2364527.2364538"},{"key":"9_CR44","doi-asserted-by":"publisher","unstructured":"Mokhov, A., Lukyanov, G., Marlow, S., Dimino, J.: Selective applicative functors. Proc. ACM Program. Lang. 3(ICFP), 90:1\u201390:29 (2019). https:\/\/doi.org\/10.1145\/3341694","DOI":"10.1145\/3341694"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Mokhov, A., Mitchell, N., Peyton\u00a0Jones, S.: Build systems \u00e0 la carte. Proc. ACM Program. Lang. 2(ICFP), 79:1\u201379:29 (2018). https:\/\/doi.org\/10.1145\/3236774","DOI":"10.1145\/3236774"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"Orso, A., Shi, N., Harrold, M.J.: Scaling regression testing to large software systems. In: International Symposium on Foundations of Software Engineering. pp. 241\u2013251. ACM, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1041685.1029928","DOI":"10.1145\/1041685.1029928"},{"key":"9_CR47","unstructured":"Palmskog, K., Celik, A., Gligoric, M.: Chip code release 1.0, https:\/\/github.com\/palmskog\/chip\/releases\/tag\/v1.0, last accessed 20 Feb 2020"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Pollock, L.L., Soffa, M.L.: Incremental compilation of optimized code. In: Symposium on Principles of Programming Languages. pp. 152\u2013164. ACM, New York, NY, USA (1985). https:\/\/doi.org\/10.1145\/318593.318629","DOI":"10.1145\/318593.318629"},{"key":"9_CR49","unstructured":"Pottier, F.: Depth-first search and strong connectivity in Coq. In: Baelde, D., Alglave, J. (eds.) Journ\u00e9es francophones des langages applicatifs (JFLA). Le Val d\u2019Ajol, France (2015), https:\/\/hal.inria.fr\/hal-01096354"},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Ren, X., Shah, F., Tip, F., Ryder, B.G., Chesley, O.: Chianti: A tool for change impact analysis of Java programs. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications. pp. 432\u2013448. ACM, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1028976.1029012","DOI":"10.1145\/1028976.1029012"},{"key":"9_CR51","unstructured":"Rothermel, G.: Efficient, Effective Regression Testing Using Safe Test Selection Techniques. Ph.D. thesis, Clemson University, Clemson, SC, USA (1996)"},{"key":"9_CR52","doi-asserted-by":"publisher","unstructured":"Rothermel, G., Harrold, M.J.: A safe, efficient regression test selection technique. Transactions on Software Engineering and Methodology 6(2), 173\u2013210 (1997). https:\/\/doi.org\/10.1145\/248233.248262","DOI":"10.1145\/248233.248262"},{"key":"9_CR53","doi-asserted-by":"publisher","unstructured":"Rungta, N., Person, S., Branchaud, J.: A change impact analysis to characterize evolving program behaviors. In: International Conference on Software Maintenance. pp. 109\u2013118. IEEE Computer Society, Washington, DC, USA (2012). https:\/\/doi.org\/10.1109\/ICSM.2012.6405261","DOI":"10.1109\/ICSM.2012.6405261"},{"key":"9_CR54","unstructured":"Shal, M.: Build system rules and algorithms (2009), http:\/\/gittup.org\/tup\/build_system_rules_and_algorithms.pdf, last accessed 21 Feb 2020"},{"key":"9_CR55","doi-asserted-by":"publisher","unstructured":"Skoglund, M., Runeson, P.: Improving class firewall regression test selection by removing the class firewall. International Journal of Software Engineering and Knowledge Engineering 17(3), 359\u2013378 (2007). https:\/\/doi.org\/10.1142\/S0218194007003306","DOI":"10.1142\/S0218194007003306"},{"key":"9_CR56","unstructured":"Th\u00e9ry, L.: Formally-Proven Kosaraju\u2019s algorithm (2015), https:\/\/hal.archives-ouvertes.fr\/hal-01095533, last accessed 21 Feb 2020"},{"key":"9_CR57","doi-asserted-by":"publisher","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the Raft consensus protocol. In: Conference on Certified Programs and Proofs. pp. 154\u2013165. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2854065.2854081","DOI":"10.1145\/2854065.2854081"},{"key":"9_CR58","doi-asserted-by":"publisher","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Conference on Programming Language Design and Implementation. pp. 283\u2013294. ACM, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"9_CR59","doi-asserted-by":"publisher","unstructured":"Yoo, S., Harman, M.: Regression testing minimization, selection and prioritization: A survey. Journal of Software Testing, Verification and Reliability 22(2), 67\u2013120 (2012). https:\/\/doi.org\/10.1002\/stvr.430","DOI":"10.1002\/stvr.430"},{"key":"9_CR60","doi-asserted-by":"publisher","unstructured":"Zhang, L.: Hybrid regression test selection. In: International Conference on Software Engineering. pp. 199\u2013209. ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3180155.3180198","DOI":"10.1145\/3180155.3180198"},{"key":"9_CR61","doi-asserted-by":"publisher","unstructured":"Zhang, L., Kim, M., Khurshid, S.: FaultTracer: a spectrum-based approach to localizing failure-inducing program edits. Journal of Software: Evolution and Process 25, 1357\u20131383 (2013). https:\/\/doi.org\/10.1002\/smr.1634","DOI":"10.1002\/smr.1634"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:04:57Z","timestamp":1616436297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}