{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:27Z","timestamp":1776305307403,"version":"3.50.1"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030888053","type":"print"},{"value":"9783030888060","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-88806-0_3","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"49-76","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Backward Symbolic Execution with Loop Folding"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1132-5516","authenticated-orcid":false,"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,13]]},"reference":[{"key":"3_CR1","unstructured":"SlowBeast. https:\/\/gitlab.fi.muni.cz\/xchalup4\/slowbeast. Accessed 15 Aug 2021"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Afzal, M., et al.: VeriAbs: verification by abstraction and test generation. In: 34th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2019, pp. 1138\u20131141. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-78800-3_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Anand","year":"2008","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 367\u2013381. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_28"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Arzt, S., Rasthofer, S., Hahn, R., Bodden, E.: Using targeted symbolic execution for reducing false-positives in dataflow analysis. In: Proceedings of the 4th ACM SIGPLAN International Workshop on State of the Art in Program Analysis, SOAP@PLDI 2015, pp. 1\u20136. ACM (2015). https:\/\/doi.org\/10.1145\/2771284.2771285","DOI":"10.1145\/2771284.2771285"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: Proceedings of the 43rd Design Automation Conference, DAC 2006, pp. 1073\u20131076. ACM (2006). https:\/\/doi.org\/10.1145\/1146909.1147180","DOI":"10.1145\/1146909.1147180"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1\u201350:39 (2018). https:\/\/doi.org\/10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-68167-2_14","volume-title":"Automated Technology for Verification and Analysis","author":"Z Baranov\u00e1","year":"2017","unstructured":"Baranov\u00e1, Z., et al.: Model checking of C and C++ with DIVINE 4. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201\u2013207. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 2005, pp. 82\u201387. ACM (2005). https:\/\/doi.org\/10.1145\/1108792.1108813","DOI":"10.1145\/1108792.1108813"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-72013-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2021","unstructured":"Beyer, D.: Software verification: 10th comparative evaluation (SV-COMP 2021). In: TACAS 2021. LNCS, vol. 12652, pp. 401\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_24"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-45190-5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2020","unstructured":"Beyer, D., Dangl, M.: Software verification with PDR: an implementation of the state of the art. In: TACAS 2020. LNCS, vol. 12078, pp. 3\u201321. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-319-21690-4_42","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2015","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"},{"key":"3_CR12","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Combining k-induction with continuously-refined invariants. CoRR abs\/1502.00096 (2015). http:\/\/arxiv.org\/abs\/1502.00096"},{"issue":"5\u20136","key":"3_CR13","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. Transf. 9(5\u20136), 505\u2013525 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","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"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-47166-2_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195\u2013211. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14"},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","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","journal-title":"STTT"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-40922-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"P Bjesse","year":"2000","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 409\u2013426. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_23"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci. 173(1), 49\u201387 (1997). https:\/\/doi.org\/10.1016\/S0304-3975(96)00191-0","journal-title":"Theor. Comput. Sci."},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-78800-3_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Boonstoppel","year":"2008","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.: RWset: attacking path explosion in constraint-based test generation. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 351\u2013366. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_27"},{"issue":"4\u20135","key":"3_CR20","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects Comput. 20(4\u20135), 379\u2013405 (2008). https:\/\/doi.org\/10.1007\/s00165-008-0080-9","journal-title":"Formal Aspects Comput."},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 363\u2013374. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542517","DOI":"10.1145\/1542476.1542517"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TSE.2014.2363469","volume":"41","author":"N Chen","year":"2015","unstructured":"Chen, N., Kim, S.: STAR: stack trace based automatic crash reproduction via symbolic execution. IEEE Trans. Softw. Eng. 41(2), 198\u2013220 (2015). https:\/\/doi.org\/10.1109\/TSE.2014.2363469","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, POPL 1978, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Danthine, A., Bremer, J.: Modelling and verification of end-to-end transport protocols. Comput. Netw. (1976) 2(4), 381\u2013395 (1978). https:\/\/www.sciencedirect.com\/science\/article\/pii\/037650757890017X","DOI":"10.1016\/0376-5075(78)90017-X"},{"key":"3_CR26","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976). https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, pp. 443\u2013456. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Dinges, P., Agha, G.A.: Targeted test input generation using symbolic-concrete backward execution. In: ACM\/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 31\u201336. ACM (2014). https:\/\/doi.org\/10.1145\/2642937.2642951","DOI":"10.1145\/2642937.2642951"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-011-0124-2","volume":"39","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des. 39(1), 83\u2013113 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0124-2","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-89960-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Fedyukovich","year":"2018","unstructured":"Fedyukovich, G., Bod\u00edk, R.: Accelerating syntax-guided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_14"},{"issue":"5","key":"3_CR31","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-011-0211-0","volume":"13","author":"J Filli\u00e2tre","year":"2011","unstructured":"Filli\u00e2tre, J.: Deductive software verification. Int. J. Softw. Tools Technol. Transf. 13(5), 397\u2013403 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0211-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 191\u2013202. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-45190-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Frohn","year":"2020","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: TACAS 2020. LNCS, vol. 12078, pp. 58\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: 33rd ACM\/IEEE International Conference on Automated Software Engineering (ASE 2018), pp. 888\u2013891. ACM, New York (2018)","DOI":"10.1145\/3238147.3240481"},{"issue":"1","key":"3_CR35","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"MYR Gadelha","year":"2017","unstructured":"Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. STTT 19(1), 97\u2013114 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0407-9","journal-title":"STTT"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-030-17502-3_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MR Gadelha","year":"2019","unstructured":"Gadelha, M.R., Monteiro, F., Cordeiro, L., Nicole, D.: ESBMC v6.0: verifying C programs using k-induction and invariant inference. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 209\u2013213. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_15"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 47\u201354. ACM (2007). https:\/\/doi.org\/10.1145\/1190216.1190226","DOI":"10.1145\/1190216.1190226"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, pp. 23\u201333. ACM (2011). https:\/\/doi.org\/10.1145\/2001420.2001424","DOI":"10.1145\/2001420.2001424"},{"key":"3_CR39","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: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 43\u201356. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452\u2013466. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_41"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_22"},{"key":"3_CR42","unstructured":"Gulwani, S., Juvekar, S.: Bound analysis using backward symbolic execution. Technical report MSR-TR-2009-156, Microsoft Research (2009)"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"Computer Aided Verification","author":"A Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634\u2013640. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_48"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, pp. 148\u2013155. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102253","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-04694-0_6","volume-title":"Runtime Verification","author":"T Hansen","year":"2009","unstructured":"Hansen, T., Schachte, P., S\u00f8ndergaard, H.: State joining and splitting for the symbolic execution of binaries. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 76\u201392. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04694-0_6"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 71\u201382. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706309","DOI":"10.1145\/1706299.1706309"},{"issue":"3","key":"3_CR47","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/321832.321835","volume":"21","author":"MS Hecht","year":"1974","unstructured":"Hecht, M.S., Ullman, J.D.: Characterizations of reducible flow graphs. J. ACM 21(3), 367\u2013375 (1974). https:\/\/doi.org\/10.1145\/321832.321835","journal-title":"J. ACM"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"3_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 187\u2013202. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16"},{"key":"3_CR50","unstructured":"Holzmann, G.J.: Backward symbolic execution of protocols. In: Protocol Specification, Testing and Verification IV, Proceedings of the IFIP WG6.1 Fourth International Workshop on Protocol Specification, Testing and Verification, pp. 19\u201330. North-Holland (1984)"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 529\u2013540. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535843","DOI":"10.1145\/2535838.2535843"},{"key":"3_CR52","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-10575-8_15","volume-title":"Handbook of Model Checking","author":"R Jhala","year":"2018","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Handbook of Model Checking, pp. 447\u2013491. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, pp. 85\u201392. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886665","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"3_CR54","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Inform. 6, 133\u2013151 (1976). https:\/\/doi.org\/10.1007\/BF00268497","journal-title":"Acta Inform."},{"issue":"7","key":"3_CR55","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-25543-5_21","volume-title":"Computer Aided Verification","author":"HG Vediramana Krishnan","year":"2019","unstructured":"Vediramana Krishnan, H.G., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 367\u2013385. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_21"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 193\u2013204. ACM (2012). https:\/\/doi.org\/10.1145\/2254064.2254088","DOI":"10.1145\/2254064.2254088"},{"key":"3_CR58","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75\u201388. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"6","key":"3_CR59","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005). https:\/\/doi.org\/10.1016\/j.ipl.2004.10.015","journal-title":"Inf. Process. Lett."},{"key":"3_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-03077-7_20","volume-title":"Hardware and Software: Verification and Testing","author":"G Li","year":"2013","unstructured":"Li, G., Ghosh, I.: Lazy symbolic execution through abstraction and sub-space search. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 295\u2013310. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_20"},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: Formal Methods in Computer-Aided Design, FMCAD 2015, pp. 105\u2013111. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"3_CR62","unstructured":"Majumdar, R., Sen, K.: Latest: lazy dynamic test input generation. Technical report UCB\/EECS-2007-36, EECS Department, University of California, Berkeley (2007)"},{"key":"3_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104\u2013118. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_10"},{"key":"3_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_2"},{"key":"3_CR66","doi-asserted-by":"publisher","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to generate disjunctive invariants. In: 36th International Conference on Software Engineering, ICSE 2014, pp. 608\u2013619. ACM (2014). https:\/\/doi.org\/10.1145\/2568225.2568275","DOI":"10.1145\/2568225.2568275"},{"key":"3_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-77505-8_26","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"C Popeea","year":"2007","unstructured":"Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331\u2013345. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77505-8_26"},{"key":"3_CR68","doi-asserted-by":"publisher","unstructured":"Qiu, R., Yang, G., Pasareanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: 37th IEEE\/ACM International Conference on Software Engineering, ICSE 2015, pp. 632\u2013642. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.79","DOI":"10.1109\/ICSE.2015.79"},{"key":"3_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-662-54580-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Rocha","year":"2017","unstructured":"Rocha, W., Rocha, H., Ismail, H., Cordeiro, L., Fischer, B.: DepthK: a k-induction verifier based on invariant inference for C programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 360\u2013364. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_23"},{"issue":"2","key":"3_CR70","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2010.09.018","volume":"267","author":"P Roux","year":"2010","unstructured":"Roux, P., Delmas, R., Garoche, P.: SMT-AI: an abstract interpreter as oracle for k-induction. Electron. Notes Theor. Comput. Sci. 267(2), 55\u201368 (2010). https:\/\/doi.org\/10.1016\/j.entcs.2010.09.018","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11823230_2","volume-title":"Static Analysis","author":"S Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3\u201317. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_2"},{"key":"3_CR72","doi-asserted-by":"publisher","unstructured":"Santelices, R.A., Harrold, M.J.: Exploiting program dependencies for scalable multiple-path symbolic execution. In: Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, pp. 195\u2013206. ACM (2010). https:\/\/doi.org\/10.1145\/1831708.1831733","DOI":"10.1145\/1831708.1831733"},{"key":"3_CR73","doi-asserted-by":"publisher","unstructured":"Saxena, P., Poosankam, P., McCamant, S., Song, D.: Loop-extended symbolic execution on binary programs. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, ISSTA 2009, pp. 225\u2013236. ACM (2009). https:\/\/doi.org\/10.1145\/1572272.1572299","DOI":"10.1145\/1572272.1572299"},{"key":"3_CR74","doi-asserted-by":"publisher","unstructured":"Sen, K., Necula, G.C., Gong, L., Choi, W.: MultiSE: multi-path symbolic execution using value summaries. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015, pp. 842\u2013853. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786830","DOI":"10.1145\/2786805.2786830"},{"key":"3_CR75","unstructured":"Sharir, M., Pnueli, A., et al.: Two approaches to interprocedural data flow analysis. New York University, Courant Institute of Mathematical Sciences (1978)"},{"key":"3_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703\u2013719. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_57"},{"key":"3_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"3_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-02444-8_15","volume-title":"Automated Technology for Verification and Analysis","author":"J Slaby","year":"2013","unstructured":"Slaby, J., Strej\u010dek, J., Trt\u00edk, M.: Compact symbolic execution. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 193\u2013207. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_15"},{"issue":"3","key":"3_CR79","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1109\/TSE.2016.2584063","volume":"43","author":"H Wang","year":"2017","unstructured":"Wang, H., Liu, T., Guan, X., Shen, C., Zheng, Q., Yang, Z.: Dependence guided symbolic execution. IEEE Trans. Softw. Eng. 43(3), 252\u2013271 (2017). https:\/\/doi.org\/10.1109\/TSE.2016.2584063","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"3_CR80","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1109\/TSE.2017.2788018","volume":"45","author":"X Xie","year":"2019","unstructured":"Xie, X., Chen, B., Zou, L., Liu, Y., Le, W., Li, X.: Automatic loop summarization via path dependency analysis. IEEE Trans. Softw. Eng. 45(6), 537\u2013557 (2019). https:\/\/doi.org\/10.1109\/TSE.2017.2788018","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"3_CR81","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/TSE.2017.2659751","volume":"44","author":"Q Yi","year":"2018","unstructured":"Yi, Q., Yang, Z., Guo, S., Wang, C., Liu, J., Zhao, C.: Eliminating path redundancy via postconditioned symbolic execution. IEEE Trans. Softw. Eng. 44(1), 25\u201343 (2018). https:\/\/doi.org\/10.1109\/TSE.2017.2659751","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88806-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:23Z","timestamp":1634145923000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88806-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888053","9783030888060"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88806-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chicago, IL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/staticanalysis.org\/","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":"40","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":"18","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":"4","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":"45% - 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","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)"}}]}}