{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:47:17Z","timestamp":1742960837532,"version":"3.40.3"},"publisher-location":"Cham","reference-count":101,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031077265"},{"type":"electronic","value":"9783031077272"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-07727-2_5","type":"book-chapter","created":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T01:12:12Z","timestamp":1654045932000},"page":"63-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reusing Predicate Precision in Value Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5890-4673","authenticated-orcid":false,"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Sallai, G., Hajdu, \u00c1.: Gazer-Theta: LLVM-based verifier portfolio with BMC\/CEGAR (Competition Contribution). In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 433\u2013437. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_27","DOI":"10.1007\/978-3-030-72013-1_27"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Afzal, M., et al.: VeriAbs: Verification by abstraction and test generation. In: ASE, pp. 1138\u20131141. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 157\u2013172. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_12","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 380\u2013397. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_25","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Alhawi, O.M., Rocha, H., Gadelha, M.R., Cordeiro, L.C., de Lima Filho, E.B.: Verification and refutation of C programs based on k-induction and invariant inference. STTT 23(2), 115\u2013135 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00564-1","DOI":"10.1007\/s10009-020-00564-1"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Amme, W., M\u00f6ller, M., Adler, P.: Data flow analysis as a general concept for the transport of verifiable program annotations. Electron. Notes Theor. Comput. Sci. 176(3), 97\u2013108 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.06.019","DOI":"10.1016\/j.entcs.2006.06.019"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Aquino, A., Bianchi, F.A., Chen, M., Denaro, G., Pezz\u00e8, M.: Reusing constraint proofs in program analysis. In: ISSTA, pp. 305\u2013315. ACM (2015). https:\/\/doi.org\/10.1145\/2771783.2771802","DOI":"10.1145\/2771783.2771802"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Aquino, A., Denaro, G., Pezz\u00e8, M.: Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions. In: ICSE, pp. 427\u2013437. IEEE (2017). https:\/\/doi.org\/10.1109\/ICSE.2017.46","DOI":"10.1109\/ICSE.2017.46"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Arzt, S., Bodden, E.: Reviser: Efficiently updating IDE-\/IFDS-based data-flow analyses in response to incremental program changes. In: ICSE, pp. 288\u2013298. ACM (2014). https:\/\/doi.org\/10.1145\/2568225.2568243","DOI":"10.1145\/2568225.2568243"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA, pp. 3\u201314. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390634","DOI":"10.1145\/1390630.1390634"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3), 273\u2013291 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.012","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software verification: 10th comparative evaluation (SV-COMP 2021). In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 401\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_24","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on boolean features. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 144\u2013159. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: FSE, pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: FSE, pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 3\u201323. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 622\u2013640. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Friedberger, K.: Violation witnesses and result validation for multi-threaded programs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 449\u2013470. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_26","DOI":"10.1007\/978-3-030-61362-4_26"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: FSE, pp. 57:1\u201357:11. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: ASE, pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Information reuse for multi-goal reachability analyses. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 472\u2013491. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_26","DOI":"10.1007\/978-3-642-37036-6_26"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.-C.: FRed: Conditional model checking via reducers and folders. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 113\u2013132. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","DOI":"10.1007\/978-3-030-58768-0_7"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Beyer, D., Jakobs, M.: Cooperative verifier-based testing with CoVeriTest. STTT 23(3), 313\u2013333 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00587-8","DOI":"10.1007\/s10009-020-00587-8"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.-C., Lemberger, T.: Difference verification with conditions. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 133\u2013154. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_8","DOI":"10.1007\/978-3-030-58768-0_8"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Beyer, D., Jakobs, M., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: ICSE, pp. 1182\u20131193. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"5_CR28","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD, pp. 189\u2013197. IEEE (2010). https:\/\/ieeexplore.ieee.org\/document\/5770949\/"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 189\u2013208. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 146\u2013162. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: FSE, pp. 389\u2013399. ACM (2013). https:\/\/doi.org\/10.1145\/2491411.2491429","DOI":"10.1145\/2491411.2491429"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Beyer, D., Stefan, W.P.: Refinement selection. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 20\u201338. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_3","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Sliced path prefixes: An effective method to enable refinement selection. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 228\u2013243. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_15","DOI":"10.1007\/978-3-319-19195-9_15"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. STTT 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: MetaVal: Witness validation via verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 165\u2013177. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_10","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, M.D.S., Oliveira, B.C., Roychoudhury, A.: Partition-based regression verification. In: ICSE, pp. 302\u2013311. IEEE (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606576","DOI":"10.1109\/ICSE.2013.6606576"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 287\u2013301. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11921240_20","DOI":"10.1007\/11921240_20"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Ja\u0161ek, T., Nov\u00e1k, J., \u0158echt\u00e1\u010dkov\u00e1, A., \u0160okov\u00e1, V., Strej\u010dek, J.: Symbiotic 8: Beyond symbolic execution. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 453\u2013457. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_31","DOI":"10.1007\/978-3-030-72013-1_31"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC, pp. 1284\u20131291. ACM (2012). https:\/\/doi.org\/10.1145\/2245276.2231980","DOI":"10.1145\/2245276.2231980"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 132\u2013146. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: ICSE, pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"5_CR42","doi-asserted-by":"crossref","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). http:\/\/doi.acm.org\/10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Cousot, P., et al.: Combination of abstractions in the ASTR\u00c9E static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272\u2013300. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_23","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 crash: Combining static checking and testing. In: ICSE, pp. 422\u2013431. ACM (2005). https:\/\/doi.org\/10.1145\/1062455.1062533","DOI":"10.1145\/1062455.1062533"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M.-C., Wehrheim, H.: Just test what you cannot verify! In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 100\u2013114. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Daca, P., Gupta, A., Henzinger, T.A.: Abstraction-driven concolic testing. In: Jobstmann, B., Leino, K., Rustan, M.: (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 328\u2013347. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"5_CR48","doi-asserted-by":"publisher","unstructured":"Dams, D.R., Namjoshi, K.S.: Orion: High-precision methods for static error analysis of C and C++ Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 138\u2013160. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_7","DOI":"10.1007\/11804192_7"},{"key":"5_CR49","doi-asserted-by":"publisher","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 423\u2013425. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"5_CR50","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 561\u2013579. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_39","DOI":"10.1007\/978-3-319-21690-4_39"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ASE, pp. 349\u2013360. ACM (2014). https:\/\/doi.org\/10.1145\/2642937.2642987","DOI":"10.1145\/2642937.2642987"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Ferles, K., W\u00fcstholz, V., Christakis, M., Dillig, I.: Failure-directed program trimming. In: FSE, pp. 174\u2013185. ACM (2017). https:\/\/doi.org\/10.1145\/3106237.3106249","DOI":"10.1145\/3106237.3106249"},{"key":"5_CR53","doi-asserted-by":"crossref","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: Dyta: Dynamic symbolic execution guided with static verification results. In: ICSE, pp. 992\u2013994. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985971","DOI":"10.1145\/1985793.1985971"},{"key":"5_CR54","doi-asserted-by":"crossref","unstructured":"Gerrard, M.J., Dwyer, M.B.: ALPACA: A large portfolio-based alternating conditional analysis. In: ICSE, pp. 35\u201338. IEEE\/ACM (2019). https:\/\/doi.org\/10.1109\/ICSE-Companion.2019.00032","DOI":"10.1109\/ICSE-Companion.2019.00032"},{"key":"5_CR55","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: Unleashing the power of alternation. In: POPL, pp. 43\u201356. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1707801.1706307"},{"key":"5_CR56","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC, pp. 466\u2013471. ACM (2009). https:\/\/doi.org\/10.1145\/1629911.1630034","DOI":"10.1145\/1629911.1630034"},{"key":"5_CR57","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: A new algorithm for property checking. In: FSE, pp. 117\u2013127. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"5_CR58","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: CoVEGI: Cooperative verification via externally generated invariants. In: Guerra, E., Stoelinga, M. (eds.) FASE 2021. LNCS, vol. 12649, pp. 108\u2013129. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_6","DOI":"10.1007\/978-3-030-71500-7_6"},{"key":"5_CR59","doi-asserted-by":"crossref","unstructured":"He, F., Yu, Q., Cai, L.: Efficient summary reuse for software regression verification. TSE (2020). https:\/\/doi.org\/10.1109\/TSE.2020.3021477","DOI":"10.1109\/TSE.2020.3021477"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"Helm, D., K\u00fcbler, F., Reif, M., Eichberg, M., Mezini, M.: Modular collaborative program analysis in OPAL. In: FSE, pp. 184\u2013196. ACM (2020), https:\/\/doi.org\/10.1145\/3368089.3409765","DOI":"10.1145\/3368089.3409765"},{"key":"5_CR61","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Necula, G.C., Jhala, R., Sutre, G., Majumdar, R., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526\u2013538. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_45","DOI":"10.1007\/3-540-45657-0_45"},{"key":"5_CR62","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 332\u2013358. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_16","DOI":"10.1007\/978-3-540-39910-0_16"},{"key":"5_CR63","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/565816.503279"},{"key":"5_CR64","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Kotoun, M., Peringer, P., Sokov\u00e1, V., Trt\u00edk, M., Vojnar, T.: Predator shape analysis tool suite. In: HVC, pp. 202\u2013209. LNCS 10028 (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_13","DOI":"10.1007\/978-3-319-49052-6_13"},{"key":"5_CR65","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: ASE, pp. 1\u20136. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.9","DOI":"10.1109\/ASE.2008.9"},{"key":"5_CR66","doi-asserted-by":"crossref","unstructured":"Inkumsah, K., Xie, T.: Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: ASE, pp. 297\u2013306. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.40","DOI":"10.1109\/ASE.2008.40"},{"key":"5_CR67","doi-asserted-by":"publisher","unstructured":"Jakobs, M.-C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 159\u2013174. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_12","DOI":"10.1007\/978-3-319-22969-0_12"},{"key":"5_CR68","doi-asserted-by":"crossref","unstructured":"Jakobs, M.: PEQcheck: Localized and context-aware checking of functional equivalence. In: FormaliSE, pp. 130\u2013140. IEEE (2021). https:\/\/doi.ieeecomputersociety.org\/10.1109\/FormaliSE52586.2021.00019","DOI":"10.1109\/FormaliSE52586.2021.00019"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Jakobs, M.: Replication package for article \u2018Reusing Predicate Precision in Value Analysis\u2019 In: iFM 2022 (2022). https:\/\/doi.org\/10.5281\/zenodo.5645043","DOI":"10.1007\/978-3-031-07727-2_5"},{"key":"5_CR70","doi-asserted-by":"crossref","unstructured":"Jakobs, M., Wehrheim, H.: Certification for configurable program analysis. In: SPIN, pp. 30\u201339. ACM (2014). https:\/\/doi.org\/10.1145\/2632362.2632372","DOI":"10.1145\/2632362.2632372"},{"key":"5_CR71","doi-asserted-by":"crossref","unstructured":"Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: ICSE, pp. 291\u2013300. ACM (2008). https:\/\/doi.org\/10.1145\/1368088.1368128","DOI":"10.1145\/1368088.1368128"},{"key":"5_CR72","doi-asserted-by":"crossref","unstructured":"Li, K., Reichenbach, C., Csallner, C., Smaragdakis, Y.: Residual investigation: Predictive and precise bug detection. In: ISSTA, pp. 298\u2013308. ACM (2012)","DOI":"10.1145\/2338965.2336789"},{"key":"5_CR73","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: ICSE, pp. 416\u2013426. IEEE (2007). https:\/\/doi.org\/10.1109\/ICSE.2007.41","DOI":"10.1109\/ICSE.2007.41"},{"key":"5_CR74","doi-asserted-by":"publisher","unstructured":"Mudduluru, R., Ramanathan, M.K.: Efficient incremental static analysis using path abstraction. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 125\u2013139. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_9","DOI":"10.1007\/978-3-642-54804-8_9"},{"key":"5_CR75","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119. ACM (1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"5_CR76","doi-asserted-by":"crossref","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., Torre, S.L., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: ASE, pp. 753\u2013764. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115686","DOI":"10.1109\/ASE.2017.8115686"},{"key":"5_CR77","doi-asserted-by":"crossref","unstructured":"Noller, Y., Kersten, R., Pasareanu, C.S.: Badger: Complexity analysis with fuzzing and symbolic execution. In: ISSTA, pp. 322\u2013332. ACM (2018). https:\/\/doi.org\/10.1145\/3213846.3213868","DOI":"10.1145\/3213846.3213868"},{"key":"5_CR78","doi-asserted-by":"crossref","unstructured":"Noller, Y., Pasareanu, C.S., B\u00f6hme, M., Sun, Y., Nguyen, H.L., Grunske, L.: Hy-Diff: Hybrid differential software analysis. In: ICSE, pp. 1273\u20131285. ACM (2020). https:\/\/doi.org\/10.1145\/3377811.3380363","DOI":"10.1145\/3377811.3380363"},{"key":"5_CR79","doi-asserted-by":"crossref","unstructured":"Palikareva, H., Kuchta, T., Cadar, C.: Shadow of a doubt: Testing for divergences between software versions. In: ICSE, pp. 1181\u20131192. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884845","DOI":"10.1145\/2884781.2884845"},{"key":"5_CR80","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S.G., Pasareanu, C.S.: Differential symbolic execution. In: FSE, pp. 226\u2013237. ACM (2008). https:\/\/doi.org\/10.1145\/1453101.1453131","DOI":"10.1145\/1453101.1453131"},{"key":"5_CR81","doi-asserted-by":"crossref","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI, pp. 504\u2013515. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993558","DOI":"10.1145\/1993316.1993558"},{"key":"5_CR82","doi-asserted-by":"crossref","unstructured":"Post, H., Sinz, C., Kaiser, A., Gorges, T.: Reducing false positives by combining abstract interpretation and bounded model checking. In: ASE, pp. 188\u2013197. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.29","DOI":"10.1109\/ASE.2008.29"},{"key":"5_CR83","doi-asserted-by":"crossref","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. JASE 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"5_CR84","doi-asserted-by":"crossref","unstructured":"Rose, E.: Lightweight bytecode verification. JAR 31(3\u20134), 303\u2013334 (2003). https:\/\/doi.org\/10.1023\/B:JARS.0000021015.15794.82","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"key":"5_CR85","doi-asserted-by":"publisher","unstructured":"Rothenberg, B.-C., Dietsch, D., Heizmann, M.: Incremental verification using trace abstraction. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 364\u2013382. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_22","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"5_CR86","doi-asserted-by":"publisher","unstructured":"Seidl, H., Erhard, J., Vogler, R.: Incremental abstract interpretation. In: Di Pierro, A., Malacaria, P., Nagarajan, R. (eds.) From Lambda Calculus to Cybersecurity Through Program Analysis. LNCS, vol. 12065, pp. 132\u2013148. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41103-9_5","DOI":"10.1007\/978-3-030-41103-9_5"},{"key":"5_CR87","doi-asserted-by":"publisher","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic construction of Hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230\u2013245. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40018-9_16","DOI":"10.1007\/978-3-540-40018-9_16"},{"key":"5_CR88","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD. pp. 114\u2013121. FMCAD Inc. (2012). http:\/\/ieeexplore.ieee.org\/document\/6462563\/"},{"key":"5_CR89","doi-asserted-by":"publisher","unstructured":"Sherman, E., Dwyer, M.B.: Structurally defined conditional data-flow static analysis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 249\u2013265. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"5_CR90","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: Leavens, G.T., Dwyer, M.B. (eds.) SPLASH, pp. 523\u2013536. ACM (2012). https:\/\/doi.org\/10.1145\/2384616.2384654","DOI":"10.1145\/2398857.2384654"},{"key":"5_CR91","doi-asserted-by":"crossref","unstructured":"Staats, M., Pasareanu, C.S.: Parallel symbolic execution for structural test generation. In: ISSTA, pp. 183\u2013194. ACM (2010). https:\/\/doi.org\/10.1145\/1831708.1831732","DOI":"10.1145\/1831708.1831732"},{"key":"5_CR92","doi-asserted-by":"crossref","unstructured":"Stephens, N., et al.: Driller: Augmenting fuzzing through selective symbolic execution. In: NDSS. The Internet Society (2016)","DOI":"10.14722\/ndss.2016.23368"},{"key":"5_CR93","doi-asserted-by":"publisher","unstructured":"\u0160vejda, J., Berger, P., Katoen, J.-P.: Interpretation-based violation witness validation for C: NITWIT. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 40\u201357. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_3","DOI":"10.1007\/978-3-030-45190-5_3"},{"key":"5_CR94","doi-asserted-by":"crossref","unstructured":"Szab\u00f3, T., Erdweg, S., Voelter, M.: IncA: A DSL for the definition of incremental program analyses. In: ASE, pp. 320\u2013331. ACM (2016). https:\/\/doi.org\/10.1145\/2970276.2970298","DOI":"10.1145\/2970276.2970298"},{"key":"5_CR95","doi-asserted-by":"publisher","unstructured":"Trostanetski, A., Grumberg, O., Kroening, D.: Modular demand-driven analysis of semantic difference for program versions. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 405\u2013427. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_20","DOI":"10.1007\/978-3-319-66706-5_20"},{"key":"5_CR96","doi-asserted-by":"crossref","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: Algorithm selection for software model checkers. In: MSR, pp. 132\u2013141. ACM (2014). https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"5_CR97","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: Reducing, reusing, and recycling constraints in program analysis. In: FSE, pp. 58:1\u201358:11. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393665","DOI":"10.1145\/2393596.2393665"},{"key":"5_CR98","doi-asserted-by":"crossref","unstructured":"Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: ICSM, pp. 115\u2013124. IEEE (2009). https:\/\/doi.org\/10.1109\/ICSM.2009.5306334","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"5_CR99","doi-asserted-by":"crossref","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In: ISSTA, pp. 144\u2013154. ACM (2012). https:\/\/doi.org\/10.1145\/2338965.2336771","DOI":"10.1145\/2338965.2336771"},{"key":"5_CR100","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together! In: ISSTA, pp. 145\u2013156. ACM (2006). https:\/\/doi.org\/10.1145\/1146238.1146255","DOI":"10.1145\/1146238.1146255"},{"key":"5_CR101","doi-asserted-by":"crossref","unstructured":"Yu, Q., He, F., Wang, B.: Incremental predicate analysis for regression verification. TOPLAS 4(OOPSLA), 184:1\u2013184:25 (2020). https:\/\/doi.org\/10.1145\/3428252","DOI":"10.1145\/3428252"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-07727-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T19:19:33Z","timestamp":1654629573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-07727-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031077265","9783031077272"],"references-count":101,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-07727-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lugano","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 June 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ifmconference.org\/","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":"46","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":"14","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":"2","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":"30% - 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":"4","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":"Also includes: 1 abstract of an invited talk, 2 invited papers, 7 extended abstracts of presentations accepted at PhD symposium","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)"}}]}}