{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T12:20:55Z","timestamp":1780316455326,"version":"3.54.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787089","type":"print"},{"value":"9783031787096","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78709-6_3","type":"book-chapter","created":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T04:48:36Z","timestamp":1738385316000},"page":"42-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The VeriAbs Tool Suite for\u00a0Code Verification"],"prefix":"10.1007","author":[{"given":"Priyanka","family":"Darke","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bharti","family":"Chimdyalwar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R.","family":"Venkatesh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,2,1]]},"reference":[{"key":"3_CR1","unstructured":"SV-COMP 2024 Benchmarks. http:\/\/sv-comp.sosy-lab.org\/2024\/benchmarks.php"},{"key":"3_CR2","unstructured":"SV-COMP Benchmarks Repository. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/tree\/svcomp22"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Schuele, T., Schneider, K.: Bounded model checking of infinite state systems: exploiting the automata hierarchy. In: MEMOCODE \u201904, pp. 17\u201326, Washington, DC, USA. IEEE Computer Society (2004)","DOI":"10.1109\/MEMCOD.2004.1459809"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Afzal, M., et al.: VeriAbs: verification by abstraction and test generation. In: ASE, pp. 1138\u20131141 (2019)","DOI":"10.1109\/ASE.2019.00121"},{"key":"3_CR5","unstructured":"Baier, D., et al.: CPAchecker 2.3 with strategy selection. In: Finkbeiner, B., Kov\u00e1cs, L., (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham (2024)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: CAV, pp. 622\u2013640 (2015)","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: CPA-DF: a tool for configurable interval analysis to boost program verification. In: 38th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2023, Luxembourg, September 11-15, 2023, pp. 2050\u20132053. IEEE (2023)","DOI":"10.1109\/ASE56229.2023.00213"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on Boolean features - a simple but effective approach. In: ISoLA (2). LNCS, vol. 11245, pages 144\u2013159. Springer (2018)","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: 23rd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2008), 15-19 September 2008, L\u2019Aquila, Italy, pp. 29\u201338. IEEE Computer Society (2008)","DOI":"10.1109\/ASE.2008.13"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: on-demand composition of cooperative verification systems. In: Fisman, D., Rosu, G. (eds.) TACAS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. LNCS, vol. 13243, pp. 561\u2013579. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: Johnsen, E.B., Wimmer, M. (eds) FASE 2022, Munich, Germany, April 2-7, 2022, Proceedings. LNCS, vol. 13241, pp. 49\u201370. Springer (2022)","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"3_CR12","unstructured":"Beyer, D., Erkan Keremoglu, M., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pp. 189\u2013197. IEEE (2010)"},{"key":"3_CR13","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and sat-based model checking revisited: adoption to software verification. arXiv preprint arXiv:2208.05046 (2022)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lemberger, T.: CPA-SymExec: efficient symbolic execution in CPAchecker. In: Huchard, M., K\u00e4stner, C., Fraser, G. (eds.) Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pp. 900\u2013903. ACM (2018)","DOI":"10.1145\/3238147.3240478"},{"key":"3_CR15","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) Fundamental Approaches to Software Engineering - 16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. LNCS, vol. 7793, pp. 146\u2013162. Springer (2013)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs by tiling. In: International Static Analysis Symposium, pp. 428\u2013449. Springer (2017)","DOI":"10.1007\/978-3-319-66706-5_21"},{"key":"3_CR17","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 22\u201339. Springer (2020)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Computer Aided Verification (CAV), pp. 911\u2013935. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_42"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Mihalkovic, V., Recht\u00e1ckov\u00e1, A., Zaoral, L., Strejcek, J.: Symbiotic 9: string analysis and backward symbolic execution with loop folding - (competition contribution). In: Fisman, D., Rosu, G. (eds.) 28th TACAS. LNCS, vol. 13244, pp. 462\u2013467. Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_32"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Chimdyalwar, B., Darke, P., Chauhan, A., Shah, P., Kumar, S., Venkatesh, R.: VeriAbs: verification by abstraction (competition contribution). In: TACAS (2017)","DOI":"10.1007\/978-3-662-54580-5_32"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Chimdyalwar, B., Darke, P., Chavda, A., Vaghani, S., Chauhan, A.: Eliminating static analysis false positives using loop abstraction and bounded model checking. In: FM, pp. 573\u2013576 (2015)","DOI":"10.1007\/978-3-319-19249-9_35"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Clarke, E. Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Darke, P., Agrawal, S., Venkatesh, R.:VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: Proceedings TACAS (2). LNCS, vol. 12652. Springer (2021)","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Agrawal, S., Kumar, S., Venkatesh, R., Chakraborty, S. VeriAbsL: scalable verification by abstraction and strategy prediction (competition contribution). In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th TACAS 2023 Paris, France, April 22-27, 2023, Proceedings, Part II. LNCS, pp. 588\u2013593. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_41"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: DATE, pp. 1407\u20131412 (2015)","DOI":"10.7873\/DATE.2015.0245"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Darke, P., Khanzode, M., Nair, A., Shrotri, U., Venkatesh, R.: Precise analysis of large industry code. In: APSEC (2012)","DOI":"10.1109\/APSEC.2012.97"},{"key":"3_CR27","unstructured":"Darke, P., Shah, T., Venkatesh, R.: A refinement to loop abstraction for bounded model checking. In: TCS Internal Technical Report (2018)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Chauhan, A., Venkatesh, R.: Efficient safety proofs for industry-scale code using abstractions and bounded model checking. In: ICST (2017)","DOI":"10.1109\/ICST.2017.53"},{"key":"3_CR29","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Knoop, J., Zdun, U. (eds.) Software Engineering 2016, pp. 67\u201368, Bonn. Gesellschaft f\u00fcr Informatik e.V (2016)"},{"issue":"1","key":"3_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40537-020-00305-w","volume":"7","author":"JT Hancock","year":"2020","unstructured":"Hancock, J.T., Khoshgoftaar, T.M.: Survey on categorical data for neural networks. J. Big Data 7(1), 1\u201341 (2020). https:\/\/doi.org\/10.1186\/s40537-020-00305-w","journal-title":"J. Big Data"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Heizmann, M., et al.: Ultimate automizer and the search for perfect interpolants - (competition contribution). In: TACAS, vol. 2, pp. 447\u2013451 (2018)","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Heizmann, M., et al.: Ultimate automizer and the search for perfect interpolants, pp. 447\u2013451 (2018)","DOI":"10.1007\/978-3-319-89963-3_30"},{"issue":"4S","key":"3_CR33","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/2641638.2641655","volume":"49","author":"TA Henzinger","year":"2014","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. ACM SIGPLAN Notices 49(4S), 79\u201391 (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA, pp. 187\u2013202. Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: Computer Aided Verification (CAV). LNCS, vol. 8044. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_26"},{"key":"3_CR36","unstructured":"Kumar, S.: Scaling up property checking (2019). https:\/\/www.cse.iitb.ac.in\/~as\/thesis_soft.pdf"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Kumar, S., Afzal, M., Venkatesh, R.: Property checking array programs using array pruning. In: TCS Internal Technical Report (2018)","DOI":"10.1007\/978-3-319-89960-2_12"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Kumar, S., Chimdyalwar, B., Shrotri, U.: Precise range analysis on large industry code. In: ESEC\/FSE, pp. 675\u2013678 (2013)","DOI":"10.1145\/2491411.2494569"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: TACAS (2018)","DOI":"10.1007\/978-3-319-89960-2_12"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Leeson, W., Dwyer, W.B.: Graves-CPA: a graph-attention verifier selector (competition contribution). In: Fisman, D., Rosu, G. (eds.) TACAS, pp. 440\u2013445. Springer, Cham (2022)","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Prabhu, S., Madhukar, K., Venkatesh, R.: Efficiently learning safety proofs from appearance as well as behaviours. In: SAS (2018)","DOI":"10.1007\/978-3-319-99725-4_20"},{"key":"3_CR42","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10515-020-00270-x","volume":"27","author":"C Richter","year":"2020","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.-C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27, 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","journal-title":"Autom. Softw. Eng."},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Richter, C., Wehrheim, H.: Attend and represent: a novel view on algorithm selection for software verification. In: ASE, pp. 1016\u20131028 (2020)","DOI":"10.1145\/3324884.3416633"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Tulsian, V., Kanade, V., Kumar, R., Lal, A., Nori, A.V.: MUX: algorithm selection for software model checkers. In: Devanbu, P., Kim, S., Pinzger, M. (eds.) 11th MSR 2014, Proceedings, May 31 - June 1, 2014, Hyderabad, India, pp. 132\u2013141. ACM (2014)","DOI":"10.1145\/2597073.2597080"},{"key":"3_CR45","unstructured":"Zhang, A., Lipton, Z.C., Li, M., Smola, A.J.: Dive into Deep Learning. Cambridge University Press (2023). https:\/\/D2L.ai"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78709-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T04:49:17Z","timestamp":1738385357000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78709-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787089","9783031787096"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78709-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}