Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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–755. ACM, New York, NY, USA (2011). https://doi.org/10.1145/1985793.1985898
Appel, A.W.: Efficient verified red-black trees (2011), https://www.cs.princeton.edu/~appel/papers/redblack.pdf, last accessed 21 Feb 2020
Arnold, R.S.: Software Change Impact Analysis. IEEE Computer Society, Los Alamitos, CA, USA (1996)
Arnold, R.S., Bohner, S.A.: Impact analysis - towards a framework for comparison. In: International Conference on Software Maintenance. pp. 292–301. IEEE Computer Society, Washington, DC, USA (1993). https://doi.org/10.1109/ICSM.1993.366933
Bazel team: Bazel Blog, https://blog.bazel.build, last accessed 20 Feb 2020
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: the calculus of inductive constructions. Springer, Heidelberg, Germany (2004). https://doi.org/10.1007/978-3-662-07964-5
Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) International Conference on Theorem Proving in Higher Order Logics. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg, Germany (2008). https://doi.org/10.1007/978-3-540-71067-7_11
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–276. ACM, New York, NY, USA (2005). https://doi.org/10.1145/1080091.1080123
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg, Germany (1997). https://doi.org/10.1007/BFb0014565
Cai, H., Santelices, R.: A comprehensive study of the predictive accuracy of dynamic change-impact analysis. J. Syst. Softw. 103(C), 248–265 (2015). https://doi.org/10.1016/j.jss.2015.02.018
Celik, A., Palmskog, K., Gligoric, M.: iCoq: Regression proof selection for large-scale verification projects. In: International Conference on Automated Software Engineering. pp. 171–182. IEEE Computer Society, Washington, DC, USA (2017). https://doi.org/10.1109/ASE.2017.8115630
Celik, A., Palmskog, K., Gligoric, M.: A regression proof selection tool for Coq. In: International Conference on Software Engineering, Tool Demonstrations. pp. 117–120. ACM, New York, NY, USA (2018). https://doi.org/10.1145/3183440.3183493
Chen, R., Cohen, C., Lévy, J.J., Merz, S., Théry, L.: Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) International Conference on Interactive Theorem Proving. pp. 13:1–13:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.13
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
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. 8442, pp. 643–657. Springer, Cham, Switzerland (2014). https://doi.org/10.1007/978-3-319-06410-9_43
Cohen, C., Théry, L.: Formalization of Tarjan 72 algorithm in Coq with Mathematical Components and SSReflect, https://github.com/CohenCyril/tarjan, last accessed 21 Feb 2020
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2), 95–120 (1988). https://doi.org/10.1016/0890-5401(88)90005-3
Coquand, T., Paulin-Mohrin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) International Conference on Computer Logic. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg, Germany (1990). https://doi.org/10.1007/3-540-52335-9_47
Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electronic Notes in Theoretical Computer Science 151(1), 75–91 (2006). https://doi.org/10.1016/j.entcs.2005.11.024
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
Esfahani, H., Fietz, J., Ke, Q., Kolomiets, A., Lan, E., Mavrinac, E., Schulte, W., Sanches, N., Kandula, S.: CloudBuild: Microsoft’s distributed and caching build service. In: International Conference on Software Engineering, Software Engineering in Practice. pp. 11–20. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2889160.2889222
ExtLib team: OCaml Extended standard Library, https://github.com/ygrek/ocaml-extlib, last accessed 20 Feb 2020
Filliâtre, J.C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) European Symposium on Programming. LNCS, vol. 2986, pp. 370–384. Springer, Heidelberg, Germany (2004). https://doi.org/10.1007/978-3-540-24725-8_26
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–343. ACM, New York, NY, USA (2017). https://doi.org/10.1145/3064176.3064183
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. 5674, pp. 327–342. Springer, Heidelberg, Germany (2009). https://doi.org/10.1007/978-3-642-03359-9_23
Gligoric, M., Eloussi, L., Marinov, D.: Practical regression test selection with dynamic file dependencies. In: International Symposium on Software Testing and Analysis. pp. 211–222. ACM, New York, NY, USA (2015). https://doi.org/10.1145/2771783.2771784
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–616. ACM, New York, NY, USA (2014). https://doi.org/10.1145/2714064.2660239
Gonthier, G.: Formal proof—the four-color theorem. Notices of the American Mathematical Society 55(11), 1382–1393 (2008), http://www.ams.org/notices/200811/tx081101382p.pdf
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, 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. 7998, pp. 163–179. Springer, Heidelberg, Germany (2013). https://doi.org/10.1007/978-3-642-39634-2_14
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3(2), 95–152 (2010). https://doi.org/10.6092/issn.1972-5787/1979
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–175. ACM, New York, NY, USA (2011). https://doi.org/10.1145/2034773.2034798
Guéneau, A., Jourdan, J.H., Charguéraud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) International Conference on Interactive Theorem Proving. pp. 18:1–18:20. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.18
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–623. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2983990.2983996
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–204. ACM, New York, NY, USA (2010). https://doi.org/10.1145/1882362.1882405
Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: Conference on Certified Programs and Proofs. pp. 137–146. ACM, New York, NY, USA (2015). https://doi.org/10.1145/2676724.2693165
Law, J., Rothermel, G.: Whole program path-based dynamic impact analysis. In: International Conference on Software Engineering. pp. 308–318. IEEE Computer Society, Washington, DC, USA (2003). https://doi.org/10.1109/ICSE.2003.1201210
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–594. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2950290.2950361
Lehnert, S.: A review of software change impact analysis. Tech. rep., Technische Universität Ilmenau, Ilmenau, Germany (2011), https://nbn-resolving.org/urn:nbn:de:gbv:ilm1-2011200618
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814
Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg, Germany (2003). https://doi.org/10.1007/3-540-39185-1_12
Luo, Q., Hariri, F., Eloussi, L., Marinov, D.: An empirical analysis of flaky tests. In: International Symposium on Foundations of Software Engineering. pp. 643–653. ACM, New York, NY, USA (2014). https://doi.org/10.1145/2635868.2635920
MathComp team: Mathematical Components project, https://math-comp.github.io, last accessed 20 Feb 2020
Mitchell, N.: Shake before building: Replacing Make with Haskell. In: International Conference on Functional Programming. pp. 55–66. ACM, New York, NY, USA (2012). https://doi.org/10.1145/2364527.2364538
Mokhov, A., Lukyanov, G., Marlow, S., Dimino, J.: Selective applicative functors. Proc. ACM Program. Lang. 3(ICFP), 90:1–90:29 (2019). https://doi.org/10.1145/3341694
Mokhov, A., Mitchell, N., Peyton Jones, S.: Build systems à la carte. Proc. ACM Program. Lang. 2(ICFP), 79:1–79:29 (2018). https://doi.org/10.1145/3236774
Orso, A., Shi, N., Harrold, M.J.: Scaling regression testing to large software systems. In: International Symposium on Foundations of Software Engineering. pp. 241–251. ACM, New York, NY, USA (2004). https://doi.org/10.1145/1041685.1029928
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
Pollock, L.L., Soffa, M.L.: Incremental compilation of optimized code. In: Symposium on Principles of Programming Languages. pp. 152–164. ACM, New York, NY, USA (1985). https://doi.org/10.1145/318593.318629
Pottier, F.: Depth-first search and strong connectivity in Coq. In: Baelde, D., Alglave, J. (eds.) Journées francophones des langages applicatifs (JFLA). Le Val d’Ajol, France (2015), https://hal.inria.fr/hal-01096354
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–448. ACM, New York, NY, USA (2004). https://doi.org/10.1145/1028976.1029012
Rothermel, G.: Efficient, Effective Regression Testing Using Safe Test Selection Techniques. Ph.D. thesis, Clemson University, Clemson, SC, USA (1996)
Rothermel, G., Harrold, M.J.: A safe, efficient regression test selection technique. Transactions on Software Engineering and Methodology 6(2), 173–210 (1997). https://doi.org/10.1145/248233.248262
Rungta, N., Person, S., Branchaud, J.: A change impact analysis to characterize evolving program behaviors. In: International Conference on Software Maintenance. pp. 109–118. IEEE Computer Society, Washington, DC, USA (2012). https://doi.org/10.1109/ICSM.2012.6405261
Shal, M.: Build system rules and algorithms (2009), http://gittup.org/tup/build_system_rules_and_algorithms.pdf, last accessed 21 Feb 2020
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–378 (2007). https://doi.org/10.1142/S0218194007003306
Théry, L.: Formally-Proven Kosaraju’s algorithm (2015), https://hal.archives-ouvertes.fr/hal-01095533, last accessed 21 Feb 2020
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–165. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2854065.2854081
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–294. ACM, New York, NY, USA (2011). https://doi.org/10.1145/1993498.1993532
Yoo, S., Harman, M.: Regression testing minimization, selection and prioritization: A survey. Journal of Software Testing, Verification and Reliability 22(2), 67–120 (2012). https://doi.org/10.1002/stvr.430
Zhang, L.: Hybrid regression test selection. In: International Conference on Software Engineering. pp. 199–209. ACM, New York, NY, USA (2018). https://doi.org/10.1145/3180155.3180198
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–1383 (2013). https://doi.org/10.1002/smr.1634
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Palmskog, K., Celik, A., Gligoric, M. (2020). Practical Machine-Checked Formalization of Change Impact Analysis. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)