{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:31:29Z","timestamp":1769751089159,"version":"3.49.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030587673","type":"print"},{"value":"9783030587680","type":"electronic"}],"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,9,8]],"date-time":"2020-09-08T00:00:00Z","timestamp":1599523200000},"content-version":"vor","delay-in-days":251,"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>\n<jats:p>Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of <jats:italic>difference verification with conditions<\/jats:italic>. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.<\/jats:p>","DOI":"10.1007\/978-3-030-58768-0_8","type":"book-chapter","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:02:48Z","timestamp":1599825768000},"page":"133-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Difference Verification with Conditions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,8]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Alt, L., Asadi, S., Chockler, H., Even-Mendoza, K., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: HiFrog: SMT-based function summarization for software verification. In: Proc. TACAS, LNCS, vol. 10206, pp. 207\u2013213. Springer (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54580-5_12","DOI":"10.1007\/978-3-662-54580-5_12"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Aquino, A., Bianchi, F.A., Chen, M., Denaro, G., Pezz\u00e8, M.: Reusing constraint proofs in program analysis. In: Proc. ISSTA, pp. 305\u2013315. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2771783.2771802","DOI":"10.1145\/2771783.2771802"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Arzt, S., Bodden, E.: Reviser: Efficiently updating IDE-\/IFDS-based data-flow analyses in response to incremental program changes. In: Proc. ICSE, pp. 288\u2013298. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2568225.2568243","DOI":"10.1145\/2568225.2568243"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Backes, J., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Proc. SPIN, LNCS, vol. 7976, pp. 99\u2013116. Springer (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39176-7_7","DOI":"10.1007\/978-3-642-39176-7_7"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: Proc. TACAS (2), LNCS, vol. 12079, pp. 347\u2013367. Springer (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45237-7_21","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on Boolean features: A simple but effective approach. In: Proc. ISoLA, LNCS, vol. 11245, pp. 144\u2013159. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV, LNCS, vol. 9206, pp. 622\u2013640. Springer (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Handbook of Model Checking, pp. 493\u2013540. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"issue":"5\u20136","key":"8_CR9","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 505\u2013525 (2007). \nhttps:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: Proc. FSE. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS, vol. 4590, pp. 504\u2013518. Springer (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T.: Replication package for article \u2018Difference verification with conditions\u2019. Zenodo (2020). \nhttps:\/\/doi.org\/10.5281\/zenodo.3954933","DOI":"10.5281\/zenodo.3954933"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proc. ICSE, pp. 1182\u20131193. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV, LNCS, vol. 6806, pp. 184\u2013190. Springer (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"8_CR15","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proc. FSE, pp. 389\u2013399. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2491411.2491429","DOI":"10.1145\/2491411.2491429"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Proc. SPIN, LNCS, vol. 9232, pp. 160\u2013178. Springer (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23404-5_12","DOI":"10.1007\/978-3-319-23404-5_12"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.scico.2013.11.026","volume":"97","author":"D Bianculli","year":"2015","unstructured":"Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: Syntactic-semantic incrementality for agile verification. SCICO 97, 47\u201354 (2015). \nhttps:\/\/doi.org\/10.1016\/j.scico.2013.11.026","journal-title":"SCICO"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"B\u00f6hme, M., Oliveira, B.C.d.S., Roychoudhury, A.: Partition-based regression verification. In: Proc. ICSE, pp. 302\u2013311. IEEE (2013). \nhttps:\/\/doi.org\/10.1109\/ICSE.2013.6606576","DOI":"10.1109\/ICSE.2013.6606576"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Carroll, M.D., Ryder, B.G.: Incremental data-flow analysis via dominator and attribute updates. In: Proc. POPL, pp. 274\u2013284. ACM (1988). \nhttps:\/\/doi.org\/10.1145\/73560.73584","DOI":"10.1145\/73560.73584"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"\u00c7elik, A., Palmskog, K., Gligoric, M.: iCoq: Regression proof selection for large-scale verification projects. In: Proc. ASE, pp. 171\u2013182. IEEE (2017). \nhttps:\/\/doi.org\/10.1109\/ASE.2017.8115630","DOI":"10.1109\/ASE.2017.8115630"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"\u00c7elik, A., Palmskog, K., Gligoric, M.: A regression proof selection tool for Coq. In: Proc. ICSE (Companion Volume), pp. 117\u2013120. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3183440.3183493","DOI":"10.1145\/3183440.3183493"},{"issue":"3","key":"8_CR23","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10703-015-0237-0","volume":"47","author":"S Chaki","year":"2015","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). FMSD 47(3), 287\u2013301 (2015). \nhttps:\/\/doi.org\/10.1007\/s10703-015-0237-0","journal-title":"FMSD"},{"issue":"5","key":"8_CR24","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). \nhttps:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: Incremental upgrade checker for C. In: Proc. TACAS, LNCS, vol. 7795, pp. 292\u2013307. Springer (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_21","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Proc. ASE, pp. 349\u2013360. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2642937.2642987","DOI":"10.1145\/2642937.2642987"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Proc. DAC, pp. 466\u2013471. ACM (2009). \nhttps:\/\/doi.org\/10.1145\/1629911.1630034","DOI":"10.1145\/1629911.1630034"},{"issue":"3","key":"8_CR28","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/stvr.1472","volume":"23","author":"B Godlin","year":"2013","unstructured":"Godlin, B., Strichman, O.: Regression verification: Proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241\u2013258 (2013). \nhttps:\/\/doi.org\/10.1002\/stvr.1472","journal-title":"Softw. Test. Verif. Reliab."},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Chen, Y.F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate Automizer and the search for perfect interpolants (competition contribution). In: Proc. TACAS (2), LNCS, vol. 10806, pp. 447\u2013451. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proc. SAS, LNCS, vol. 5673, pp. 69\u201385. Springer (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03237-0_7","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV, LNCS, vol. 8044, pp. 36\u201352. Springer (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232\u2013244. ACM (2004). \nhttps:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Verification: Theory and Practice, LNCS, vol. 2772, pp. 332\u2013358 (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-39910-0_16","DOI":"10.1007\/978-3-540-39910-0_16"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM (2002). \nhttps:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Jackson, D., Ladd, D.A.: Semantic Diff: A tool for summarizing the effects of modifications. In: Proc. ICSM, pp. 243\u2013252. IEEE (1994). \nhttps:\/\/doi.org\/10.1109\/ICSM.1994.336770","DOI":"10.1109\/ICSM.1994.336770"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Jia, X., Ghezzi, C., Ying, S.: Enhancing reuse of constraint solutions to improve symbolic execution. In: Proc. ISSTA, pp. 177\u2013187. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2771783.2771806","DOI":"10.1145\/2771783.2771806"},{"key":"8_CR37","unstructured":"Kawaguchi, M., Lahiri, S., Rebelo, H.: Conditional equivalence. Tech. rep., Microsoft Research (2010)"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Proc. FSE, pp. 345\u2013355. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2491411.2491452","DOI":"10.1145\/2491411.2491452"},{"issue":"4","key":"8_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/DagRep.8.4.1","volume":"8","author":"SK Lahiri","year":"2018","unstructured":"Lahiri, S.K., Murawski, A., Strichman, O., Ulbrich, M.: Program Equivalence (Dagstuhl Seminar 18151). Dagstuhl Reports 8(4), 1\u201319 (2018). \nhttps:\/\/doi.org\/10.4230\/DagRep.8.4.1","journal-title":"Dagstuhl Reports"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: Opportunities, applications, and challenges. In: Proc. FoSER, pp. 201\u2013204. ACM (2010). \nhttps:\/\/doi.org\/10.1145\/1882362.1882405","DOI":"10.1145\/1882362.1882405"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: Proc. ICSE, pp. 291\u2013300. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1368088.1368128","DOI":"10.1145\/1368088.1368128"},{"key":"8_CR42","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: Fine-grained caching of verification results. In: Proc. CAV, LNCS, vol. 9206, pp. 380\u2013397. Springer (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_22","DOI":"10.1007\/978-3-319-21690-4_22"},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV, LNCS, vol. 2725, pp. 1\u201313. Springer (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Mudduluru, R., Ramanathan, M.K.: Efficient incremental static analysis using path abstraction. In: Proc. FASE, LNCS, vol. 8411, pp. 125\u2013139. Springer (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54804-8_9","DOI":"10.1007\/978-3-642-54804-8_9"},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"Partush, N., Yahav, E.: Abstract semantic differencing for numerical programs. In: Proc. SAS, LNCS, vol. 7935, pp. 238\u2013258. Springer (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38856-9_14","DOI":"10.1007\/978-3-642-38856-9_14"},{"key":"8_CR46","doi-asserted-by":"publisher","unstructured":"Person, S., Dwyer, M.B., Elbaum, S.G., P\u0103s\u0103reanu, C.S.: Differential symbolic execution. In: Proc. FSE, pp. 226\u2013237. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1453101.1453131","DOI":"10.1145\/1453101.1453131"},{"key":"8_CR47","doi-asserted-by":"publisher","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Proc. PLDI, pp. 504\u2013515. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1993498.1993558","DOI":"10.1145\/1993498.1993558"},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Proc. CAV, LNCS, vol. 6806, pp. 669\u2013685. Springer (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_55","DOI":"10.1007\/978-3-642-22110-1_55"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Rothenberg, B., Dietsch, D., Heizmann, M.: Incremental verification using trace abstraction. In: Proc. SAS, LNCS, vol. 11002, pp. 364\u2013382. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-99725-4_22","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Rungta, N., Person, S., Branchaud, J.: A change impact analysis to characterize evolving program behaviors. In: Proc. ICSM, pp. 109\u2013118. IEEE (2012). \nhttps:\/\/doi.org\/10.1109\/ICSM.2012.6405261","DOI":"10.1109\/ICSM.2012.6405261"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Ryder, B.G.: Incremental data-flow analysis. In: Proc. POPL, pp. 167\u2013176. ACM (1983). \nhttps:\/\/doi.org\/10.1145\/567067.567084","DOI":"10.1145\/567067.567084"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Seidl, H., Erhard, J., Vogler, R.: Incremental abstract interpretation. In: From Lambda Calculus to Cybersecurity Through Program Analysis - Essays Dedicated to Chris Hankin on the Occasion of His Retirement, LNCS, vol. 12065, pp. 132\u2013148. Springer (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-41103-9_5","DOI":"10.1007\/978-3-030-41103-9_5"},{"key":"8_CR53","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: Proc. FMCAD, pp. 114\u2013121. FMCAD Inc. (2012)"},{"key":"8_CR54","doi-asserted-by":"publisher","unstructured":"Sokolsky, O.V., Smolka, S.A.: Incremental model checking in the modal mu-calculus. In: Proc. CAV, LNCS, vol. 818, pp. 351\u2013363. Springer (1994). \nhttps:\/\/doi.org\/10.1007\/3-540-58179-0_67","DOI":"10.1007\/3-540-58179-0_67"},{"key":"8_CR55","doi-asserted-by":"publisher","unstructured":"Strichman, O., Godlin, B.: Regression verification \u2013 a practical way to verify programs. In: Proc. VSTTE, LNCS, vol. 4171, pp. 496\u2013501. Springer (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69149-5_54","DOI":"10.1007\/978-3-540-69149-5_54"},{"key":"8_CR56","doi-asserted-by":"publisher","unstructured":"Strichman, O., Veitsman, M.: Regression verification for unbalanced recursive functions. In: Proc. FM, LNCS, vol. 9995, pp. 645\u2013658 (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_39","DOI":"10.1007\/978-3-319-48989-6_39"},{"key":"8_CR57","doi-asserted-by":"publisher","unstructured":"Szab\u00f3, T., Bergmann, G., Erdweg, S., Voelter, M.: Incrementalizing lattice-based program analyses in Datalog. PACMPL 2(OOPSLA), 139:1\u2013139:29 (2018). \nhttps:\/\/doi.org\/10.1145\/3276509","DOI":"10.1145\/3276509"},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"Szab\u00f3, T., Erdweg, S., Voelter, M.: IncA: A DSL for the definition of incremental program analyses. In: Proc. ASE, pp. 320\u2013331. ACM (2016). \nhttps:\/\/doi.org\/10.1145\/2970276.2970298","DOI":"10.1145\/2970276.2970298"},{"key":"8_CR59","doi-asserted-by":"publisher","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: Reducing, reusing, and recycling constraints in program analysis. In: Proc. FSE, pp. 58:1\u201358:11. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2393596.2393665","DOI":"10.1145\/2393596.2393665"},{"key":"8_CR60","doi-asserted-by":"publisher","unstructured":"Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: Proc. ICSM, pp. 115\u2013124. IEEE (2009). \nhttps:\/\/doi.org\/10.1109\/ICSM.2009.5306334","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"8_CR61","doi-asserted-by":"publisher","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In: Proc. ISSTA, pp. 144\u2013154. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2338965.2336771","DOI":"10.1145\/2338965.2336771"},{"issue":"2","key":"8_CR62","first-page":"67","volume":"22","author":"S Yoo","year":"2012","unstructured":"Yoo, S., Harman, M.: Regression testing minimization, selection, and prioritization: A survey. STVR 22(2), 67\u2013120 (2012). \nhttps:\/\/onlinelibrary.wiley.com\/doi\/abs\/10.1002\/stvr.430","journal-title":"STVR"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58768-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:05:19Z","timestamp":1599825919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58768-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030587673","9783030587680"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58768-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}