{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:47:51Z","timestamp":1769752071803,"version":"3.49.0"},"publisher-location":"Cham","reference-count":98,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308253","type":"print"},{"value":"9783031308260","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Ranged symbolic execution<\/jats:italic> has been proposed as a way of scaling symbolic execution by splitting the task of path exploration onto several workers running in parallel. The split is conducted along path <jats:italic>ranges<\/jats:italic> which \u2013 simply speaking \u2013 describe sets of paths. Workers can then explore path ranges in parallel.<\/jats:p><jats:p>In this paper, we propose <jats:italic>ranged analysis<\/jats:italic> as the generalization of ranged symbolic execution to arbitrary program analyses. This allows us to not only parallelize a single analysis, but also run <jats:italic>different<\/jats:italic> analyses on different ranges of a program in parallel. Besides this generalization, we also provide a novel <jats:italic>range splitting<\/jats:italic> strategy operating along loop bounds, complementing the existing random strategy of the original proposal. We implemented ranged analysis within the tool <jats:sc>CPAchecker<\/jats:sc> and evaluated it on programs from the SV-COMP benchmark. The evaluation in particular shows the superiority of loop bounds splitting over random splitting. We furthermore find that compositions of ranged analyses can solve analysis tasks that none of the constituent analysis alone can solve.<\/jats:p>","DOI":"10.1007\/978-3-031-30826-0_11","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T18:02:59Z","timestamp":1681927379000},"page":"195-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Parallel Program Analysis via Range Splitting"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5098-0495","authenticated-orcid":false,"given":"Jan","family":"Haltermann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5890-4673","authenticated-orcid":false,"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2906-6508","authenticated-orcid":false,"given":"Cedric","family":"Richter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Proc. TACAS. pp. 157\u2013172. LNCS\u00a07214, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_12","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Avgerinos, T., Rebert, A., Cha, S.K., Brumley, D.: Enhancing symbolic execution with veritesting. In: Proc. ICSE. pp. 1083\u20131094. ACM (2014), https:\/\/doi.org\/10.1145\/2568225.2568293","DOI":"10.1145\/2568225.2568293"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Baars, A.I., Harman, M., Hassoun, Y., Lakhotia, K., McMinn, P., Tonella, P., Vos, T.E.J.: Symbolic search-based testing. In: Proc. ASE. pp. 53\u201362. IEEE (2011). https:\/\/doi.org\/10.1109\/ASE.2011.6100119","DOI":"10.1109\/ASE.2011.6100119"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Baluda, M.: EvoSE: Evolutionary symbolic execution. In: Proc. A-TEST. pp. 16\u201319. ACM (2015), https:\/\/doi.org\/10.1145\/2804322.2804325","DOI":"10.1145\/2804322.2804325"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Beckman, N., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proc. ISSTA. pp. 3\u201314. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390634","DOI":"10.1145\/1390630.1390634"},{"key":"11_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. pp. 144\u2013159. LNCS\u00a011245, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV. pp. 622\u2013640. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"11_CR8","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). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE. pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.: CoVeriTest: Cooperative verifier-based testing. In: Proc. FASE. pp. 389\u2013408. LNCS\u00a011424, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Jakobs, M., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proc. ICSE. pp. 1182\u20131193. ACM (2018), https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: Off-the-shelf combination of test-case generators. In: Proc. ATVA. pp. 189\u2013208. LNCS\u00a011781, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: TACAS. Lecture Notes in Computer Science, vol. 13244, pp. 375\u2013402. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20_20.","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Proc. FSE. pp. 326\u2013337. ACM (2016), https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299\u2013335 (2018), https:\/\/doi.org\/10.1007\/s10817-017-9432-6","DOI":"10.1007\/s10817-017-9432-6"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Haltermann, J., Lemberger, T., Wehrheim, H.: Decomposing software verification into off-the-shelf components: An application to CEGAR. In: Proc. ICSE. ACM (2022). https:\/\/doi.org\/10.1145\/3510003.351006","DOI":"10.1145\/3510003.351006"},{"key":"11_CR17","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. pp. 504\u2013518. LNCS\u00a04590, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. (ASE. pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proc. ICSE. pp. 1182\u20131193. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S.: Coveriteam: On-demand composition of cooperative verification systems. In: Proc. TACAS. LNCS, vol. 13243, pp. 561\u2013579. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS\u00a06806, Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"11_CR22","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD. pp. 189\u2013197. IEEE (2010), https:\/\/ieeexplore.ieee.org\/document\/5770949\/"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. In: Proc. ISoLA. LNCS, vol. 12476, pp. 143\u2013167. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J., Melquiond, G.: Combining coq and gappa for certifying floating-point programs. In: Proc. MKM. pp. 59\u201374. LNCS\u00a05625, Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-02614-0_10","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Braione, P., Denaro, G., Mattavelli, A., Pezz\u00e8, M.: Combining symbolic execution and search-based testing for programs with complex heap inputs. In: Proc. ISSTA. pp. 90\u2013101. ACM (2017), https:\/\/doi.org\/10.1145\/3092703.3092715","DOI":"10.1145\/3092703.3092715"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proc. EuroSys. pp. 183\u2013198. ACM (2011), https:\/\/doi.org\/10.1145\/1966445.1966463","DOI":"10.1145\/1966445.1966463"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: Proc. SAC. pp. 1284\u20131291. ACM (2012). https:\/\/doi.org\/10.1145\/2245276.2231980","DOI":"10.1145\/2245276.2231980"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Chen, T., Heo, K., Raghothaman, M.: Boosting static analysis accuracy with instrumented test executions. In: Proc. FSE. pp. 1154\u20131165. ACM (2021), https:\/\/doi.org\/10.1145\/3468264.3468626","DOI":"10.1145\/3468264.3468626"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Chowdhury, A.B., Medicherla, R.K., Venkatesh, R.: Verifuzz: Program aware fuzzing - (competition contribution). In: Proc. TACAS, part 3. pp. 244\u2013249. LNCS\u00a011429, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_22","DOI":"10.1007\/978-3-030-17502-3_22"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Proc. ICSE. pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Christakis, M., Eniser, H.F., Hermanns, H., Hoffmann, J., Kothari, Y., Li, J., Navas, J.A., W\u00fcstholz, V.: Automated safety verification of programs invoking neural networks. In: Proc. CAV. pp. 201\u2013224. LNCS\u00a012759, Springer (2021), https:\/\/doi.org\/10.1007\/978-3-030-81685-8_9","DOI":"10.1007\/978-3-030-81685-8_9"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Proc. FM. LNCS, vol.\u00a07436, pp. 132\u2013146. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Ciortea, L., Zamfir, C., Bucur, S., Chipounov, V., Candea, G.: Cloud9: A software testing service. OSR 43(4), 5\u201310 (2009), https:\/\/doi.org\/10.1145\/1713254.1713257","DOI":"10.1145\/1713254.1713257"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. CAV. pp. 154\u2013169. LNCS\u00a01855, Springer (2000), https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"11_CR36","unstructured":"SV-Benchmarks Community: SV-Benchmarks (2022), https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/tree\/svcomp22"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Proc. POPL. pp. 269\u2013282. ACM (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the astr\u00e9e static analyzer. In: Proc. ASIAN\u201906. pp. 272\u2013300. LNCS\u00a04435, Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_23","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 crash: Combining static checking and testing. In: Proc. ICSE. pp. 422\u2013431. ACM (2005). https:\/\/doi.org\/10.1145\/1062455.1062533","DOI":"10.1145\/1062455.1062533"},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"Czech, M., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Predicting rankings of software verification tools. In: Proc. SWAN. pp. 23\u201326. ACM (2017). https:\/\/doi.org\/10.1145\/3121257.3121262","DOI":"10.1145\/3121257.3121262"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Proc. FASE. LNCS, vol.\u00a09033, pp. 100\u2013114. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"11_CR42","doi-asserted-by":"publisher","unstructured":"Daca, P., Gupta, A., Henzinger, T.A.: Abstraction-driven concolic testing. In: Proc. VMCAI. pp. 328\u2013347. LNCS\u00a09583, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"11_CR43","doi-asserted-by":"publisher","unstructured":"Dams, D., Namjoshi, K.S.: Orion: High-precision methods for static error analysis of C and C++ programs. In: Proc. FMCO. pp. 138\u2013160. LNCS\u00a04111, Springer (2005). https:\/\/doi.org\/10.1007\/11804192_7","DOI":"10.1007\/11804192_7"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: Cpachecker with support for recursive programs and floating-point arithmetic - (competition contribution). In: Proc. TACS. pp. 423\u2013425. LNCS\u00a09035, Springer (2015), https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"11_CR45","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Proc. CAV. pp. 561\u2013579. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_39","DOI":"10.1007\/978-3-319-21690-4_39"},{"key":"11_CR46","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science, Springer (1990). https:\/\/doi.org\/10.1007\/978-1-4612-3228-5","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Ferles, K., W\u00fcstholz, V., Christakis, M., Dillig, I.: Failure-directed program trimming. In: Proc. ESEC\/FSE. pp. 174\u2013185. ACM (2017), http:\/\/doi.acm.org\/10.1145\/3106237.3106249","DOI":"10.1145\/3106237.3106249"},{"key":"11_CR48","doi-asserted-by":"crossref","unstructured":"Funes, D., Siddiqui, J.H., Khurshid, S.: Ranged model checking. ACM SIGSOFT Softw. Eng. Notes 37(6), \u00a01\u20135 (2012), https:\/\/doi.org\/10.1145\/2382756.2382799","DOI":"10.1145\/2382756.2382799"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Fraser, G., Arcuri, A.: Improving search-based test suite generation with dynamic symbolic execution. In: Proc. ISSRE. pp. 360\u2013369. IEEE (2013), https:\/\/doi.org\/10.1109\/ISSRE.2013.6698889","DOI":"10.1109\/ISSRE.2013.6698889"},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"Gao, M., He, L., Majumdar, R., Wang, Z.: LLSPLAT: improving concolic testing by bounded model checking. In: Proc. SCAM. pp. 127\u2013136. IEEE (2016), https:\/\/doi.org\/10.1109\/SCAM.2016.26","DOI":"10.1109\/SCAM.2016.26"},{"key":"11_CR51","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Vavassori, P.: Using decision trees to aid algorithm selection in combinatorial interaction tests generation. In: Proc. ICST. pp. 1\u201310. IEEE (2015), https:\/\/doi.org\/10.1109\/ICSTW.2015.7107442","DOI":"10.1109\/ICSTW.2015.7107442"},{"key":"11_CR52","doi-asserted-by":"publisher","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: Dyta: Dynamic symbolic execution guided with static verification results. In: Proc. ICSE. pp. 992\u2013994. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985971","DOI":"10.1145\/1985793.1985971"},{"key":"11_CR53","doi-asserted-by":"crossref","unstructured":"Gerrard, M.J., Dwyer, M.B.: ALPACA: a large portfolio-based alternating conditional analysis. In: Proc. ICSE. pp. 35\u201338. IEEE \/ ACM (2019), https:\/\/doi.org\/10.1109\/ICSE-Companion.2019.00032","DOI":"10.1109\/ICSE-Companion.2019.00032"},{"key":"11_CR54","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proc. PLDI. pp. 213\u2013223. ACM (2005), https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1064978.1065036"},{"key":"11_CR55","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: Unleashing the power of alternation. In: Proc. POPL. pp. 43\u201356. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706307, http:\/\/doi.acm.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"11_CR56","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proc. NDSS. The Internet Society (2008), http:\/\/www.isoc.org\/isoc\/conferences\/ndss\/08\/papers\/10_automated_whitebox_fuzz.pdf"},{"key":"11_CR57","doi-asserted-by":"crossref","unstructured":"Groce, A., Zhang, C., Eide, E., Chen, Y., Regehr, J.: Swarm testing. In: Proc. ISSTA. pp. 78\u201388. ACM (2012), https:\/\/doi.org\/10.1145\/2338965.2336763","DOI":"10.1145\/2338965.2336763"},{"key":"11_CR58","doi-asserted-by":"publisher","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proc. FSE. pp. 117\u2013127. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Haltermann, J., Wehrheim, H.: CoVEGI: Cooperative Verification via Externally Generated Invariants. In: Proc. FASE. pp. 108\u2013129. LNCS\u00a012649, Springer (2021), https:\/\/doi.org\/10.1007\/978-3-030-71500-7_6","DOI":"10.1007\/978-3-030-71500-7_6"},{"key":"11_CR60","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Jakobs, M., Richter, C., Wehrheim, H.: Replication package for article \u2019Parallel Program Analysis via Range Splitting\u2019 (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7189816","DOI":"10.5281\/zenodo.7189816"},{"key":"11_CR61","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Chen, Y., 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. pp. 447\u2013451. LNCS\u00a010806, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"11_CR62","doi-asserted-by":"crossref","unstructured":"Helm, D., K\u00fcbler, F., Reif, M., Eichberg, M., Mezini, M.: Modular collaborative program analysis in OPAL. In: Proc. FSE. pp. 184\u2013196. ACM (2020), https:\/\/doi.org\/10.1145\/3368089.3409765","DOI":"10.1145\/3368089.3409765"},{"key":"11_CR63","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL. pp. 232\u2013244. ACM (2004), https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/982962.964021"},{"key":"11_CR64","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL. pp. 58\u201370. ACM (2002), https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/565816.503279"},{"key":"11_CR65","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: Proc. HVC. pp. 202\u2013209. LNCS\u00a010028 (2016), https:\/\/doi.org\/10.1007\/978-3-319-49052-6_13","DOI":"10.1007\/978-3-319-49052-6_13"},{"key":"11_CR66","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proc. ASE. pp.\u00a01\u20136. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.9","DOI":"10.1109\/ASE.2008.9"},{"key":"11_CR67","doi-asserted-by":"crossref","unstructured":"Huster, S., Str\u00f6bele, J., Ruf, J., Kropf, T., Rosenstiel, W.: Using robustness testing to handle incomplete verification results when combining verification and testing techniques. In: Proc. ICTSS. pp. 54\u201370. LNCS\u00a010533, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-67549-7_4","DOI":"10.1007\/978-3-319-67549-7_4"},{"key":"11_CR68","doi-asserted-by":"crossref","unstructured":"Inkumsah, K., Xie, T.: Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: Proc. ASE. pp. 297\u2013306. IEEE (2008), https:\/\/doi.org\/10.1109\/ASE.2008.40","DOI":"10.1109\/ASE.2008.40"},{"key":"11_CR69","doi-asserted-by":"crossref","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: Proc. PPoPP. pp. 202\u2013216. ACM (2020), https:\/\/doi.org\/10.1145\/3332466.3374529","DOI":"10.1145\/3332466.3374529"},{"key":"11_CR70","doi-asserted-by":"crossref","unstructured":"Jakobs, M.: $${PART}_{PW}$$ : From partial analysis results to a proof witness. In: Proc. SEFM. pp. 120\u2013135. LNCS\u00a010469, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-66197-1_8","DOI":"10.1007\/978-3-319-66197-1_8"},{"key":"11_CR71","doi-asserted-by":"publisher","unstructured":"Jalote, P., Vangala, V., Singh, T., Jain, P.: Program partitioning: A framework for combining static and dynamic analysis. In: Proc. WODA. pp. 11\u201316. ACM (2006). https:\/\/doi.org\/10.1145\/1138912.1138916, http:\/\/doi.acm.org\/10.1145\/1138912.1138916","DOI":"10.1145\/1138912.1138916"},{"key":"11_CR72","doi-asserted-by":"crossref","unstructured":"Jia, Y., Cohen, M.B., Harman, M., Petke, J.: Learning combinatorial interaction test generation strategies using hyperheuristic search. In: Proc. ICSE. pp. 540\u2013550. IEEE (2015), https:\/\/doi.org\/10.1109\/ICSE.2015.71","DOI":"10.1109\/ICSE.2015.71"},{"key":"11_CR73","doi-asserted-by":"crossref","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976), https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"11_CR74","doi-asserted-by":"publisher","unstructured":"Li, K., Reichenbach, C., Csallner, C., Smaragdakis, Y.: Residual investigation: Predictive and precise bug detection. In: Proc. ISSTA. pp. 298\u2013308. ACM (2012). https:\/\/doi.org\/10.1145\/2338965.2336789","DOI":"10.1145\/2338965.2336789"},{"key":"11_CR75","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proc. ICSE. pp. 416\u2013426. IEEE (2007), https:\/\/doi.org\/10.1109\/ICSE.2007.41","DOI":"10.1109\/ICSE.2007.41"},{"key":"11_CR76","doi-asserted-by":"crossref","unstructured":"Misailovic, S., Milicevic, A., Petrovic, N., Khurshid, S., Marinov, D.: Parallel test generation and execution with Korat. In: Proc. ESEC\/FSE. pp. 135\u2013144. ACM (2007), https:\/\/doi.org\/10.1145\/1287624.1287645","DOI":"10.1145\/1287624.1287645"},{"key":"11_CR77","doi-asserted-by":"publisher","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., La\u00a0Torre, S., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: Proc. ASE. pp. 753\u2013764. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115686","DOI":"10.1109\/ASE.2017.8115686"},{"key":"11_CR78","doi-asserted-by":"crossref","unstructured":"Noller, Y., Kersten, R., Pasareanu, C.S.: Badger: Complexity analysis with fuzzing and symbolic execution. In: Proc. ISSTA. pp. 322\u2013332. ACM (2018), http:\/\/doi.acm.org\/10.1145\/3213846.3213868","DOI":"10.1145\/3213846.3213868"},{"key":"11_CR79","doi-asserted-by":"crossref","unstructured":"Noller, Y., Pasareanu, C.S., B\u00f6hme, M., Sun, Y., Nguyen, H.L., Grunske, L.: Hydiff: Hybrid differential software analysis. In: Proc. ICSE. pp. 1273\u20131285. ACM (2020), https:\/\/doi.org\/10.1145\/3377811.3380363","DOI":"10.1145\/3377811.3380363"},{"key":"11_CR80","doi-asserted-by":"crossref","unstructured":"Pauck, F., Wehrheim, H.: Together strong: Cooperative android app analysis. In: Proc. ESEC\/FSE. pp. 374\u2013384. ACM (2019), https:\/\/doi.org\/10.1145\/3338906.3338915","DOI":"10.1145\/3338906.3338915"},{"key":"11_CR81","doi-asserted-by":"publisher","unstructured":"Post, H., Sinz, C., Kaiser, A., Gorges, T.: Reducing false positives by combining abstract interpretation and bounded model checking. In: Proc. ASE. pp. 188\u2013197. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.29","DOI":"10.1109\/ASE.2008.29"},{"key":"11_CR82","doi-asserted-by":"crossref","unstructured":"Qiu, R., Khurshid, S., Pasareanu, C.S., Wen, J., Yang, G.: Using test ranges to improve symbolic execution. In: Proc. NFM. pp. 416\u2013434. LNCS\u00a010811, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-77935-5_28","DOI":"10.1007\/978-3-319-77935-5_28"},{"key":"11_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":"11_CR84","doi-asserted-by":"publisher","unstructured":"Sakti, A., Gu\u00e9h\u00e9neuc, Y., Pesant, G.: Boosting search based testing by using constraint based testing. In: Proc. SSBSE. pp. 213\u2013227. LNCS\u00a07515, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33119-0_16","DOI":"10.1007\/978-3-642-33119-0_16"},{"key":"11_CR85","doi-asserted-by":"crossref","unstructured":"Sherman, E., Dwyer, M.B.: Structurally defined conditional data-flow static analysis. In: Proc. TACAS. pp. 249\u2013265. LNCS\u00a010806, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"11_CR86","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: Proc. SPLASH. pp. 523\u2013536. ACM (2012), https:\/\/doi.org\/10.1145\/2384616.2384654","DOI":"10.1145\/2398857.2384654"},{"key":"11_CR87","doi-asserted-by":"crossref","unstructured":"Singh, S., Khurshid, S.: Parallel chopped symbolic execution. In: Proc. ICFEM. pp. 107\u2013125. LNCS\u00a012531, Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-63406-3_7","DOI":"10.1007\/978-3-030-63406-3_7"},{"key":"11_CR88","unstructured":"Singh, S., Khurshid, S.: Distributed symbolic execution using test-depth partitioning. CoRR abs\/2106.02179 (2021), https:\/\/arxiv.org\/abs\/2106.02179"},{"key":"11_CR89","doi-asserted-by":"crossref","unstructured":"Staats, M., Pasareanu, S.S.: Parallel symbolic execution for structural test generation. In: Proc. ISSTA. pp. 183\u2013194. ACM (2010), https:\/\/doi.org\/10.1145\/1831708.1831732","DOI":"10.1145\/1831708.1831732"},{"key":"11_CR90","doi-asserted-by":"crossref","unstructured":"Stephens, N., Grosen, J., Salls, C., Dutcher, A., Wang, R., Corbetta, J., Shoshitaishvili, Y., Kruegel, C., Vigna, G.: Driller: Augmenting fuzzing through selective symbolic execution. In: Proc. NDSS. The Internet Society (2016), http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2017\/09\/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf","DOI":"10.14722\/ndss.2016.23368"},{"key":"11_CR91","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Proc. SEFM. pp. 382\u2013398. LNCS\u00a07041, Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-24690-6_26","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"11_CR92","doi-asserted-by":"crossref","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: Algorithm selection for software model checkers. In: Proc. MSR. p. 132\u2013141. ACM (2014), https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"11_CR93","doi-asserted-by":"crossref","unstructured":"Yang, G., Do, Q.C.D., Wen, J.: Distributed assertion checking using symbolic execution. ACM SIGSOFT Softw. Eng. Notes 40(6), \u00a01\u20135 (2015), https:\/\/doi.org\/10.1145\/2830719.2830729","DOI":"10.1145\/2830719.2830729"},{"key":"11_CR94","doi-asserted-by":"publisher","unstructured":"Yang, G., Qiu, R., Khurshid, S., Pasareanu, C.S., Wen, J.: A synergistic approach to improving symbolic execution using test ranges. Innov. Syst. Softw. Eng. 15(3-4), 325\u2013342 (2019). https:\/\/doi.org\/10.1007\/s11334-019-00331-9","DOI":"10.1007\/s11334-019-00331-9"},{"key":"11_CR95","doi-asserted-by":"crossref","unstructured":"Yin, B., Chen, L., Liu, J., Wang, J., Cousot, P.: Verifying numerical programs via iterative abstract testing. In: Proc. SAS. pp. 247\u2013267. LNCS\u00a011822, Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-32304-2_13","DOI":"10.1007\/978-3-030-32304-2_13"},{"key":"11_CR96","doi-asserted-by":"crossref","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Parallel refinement for multi-threaded program verification. In: Proc. ICSE. pp. 643\u2013653. IEEE (2019), https:\/\/doi.org\/10.1109\/ICSE.2019.00074","DOI":"10.1109\/ICSE.2019.00074"},{"key":"11_CR97","doi-asserted-by":"publisher","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together! In: Proc. ISSTA. pp. 145\u2013156. ACM (2006). https:\/\/doi.org\/10.1145\/1146238.1146255","DOI":"10.1145\/1146238.1146255"},{"key":"11_CR98","doi-asserted-by":"crossref","unstructured":"Zhou, L., Gan, S., Qin, X., Han, W.: Secloud: Binary analyzing using symbolic execution in the cloud. In: Proc. CBD. pp. 58\u201363. IEEE (2013), https:\/\/doi.org\/10.1109\/CBD.2013.31","DOI":"10.1109\/CBD.2013.31"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30826-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,22]],"date-time":"2023-05-22T22:03:10Z","timestamp":1684792990000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30826-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308253","9783031308260"],"references-count":98,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30826-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","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":"fase2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"50","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":"12","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":"0","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":"24% - 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":"6-7","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 proceedings also include 2 tool papers, 2 NIER papers, and 2 competition papers","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)"}}]}}