{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:21Z","timestamp":1774063041223,"version":"3.50.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452360","type":"print"},{"value":"9783030452377","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an array verification technique called <jats:italic>full-program induction<\/jats:italic>, and enhance the existing techniques of loop pruning, <jats:italic>k<\/jats:italic>-path interval analysis, and disjunctive loop summarization. These changes have improved the verification of programs with arrays, and unstructured loops and unstructured control flows.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_25","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"383-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)"],"prefix":"10.1007","author":[{"given":"Mohammad","family":"Afzal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7527-7675","authenticated-orcid":false,"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avriti","family":"Chauhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bharti","family":"Chimdyalwar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Priyanka","family":"Darke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shrawan","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Babu M","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6106-4719","authenticated-orcid":false,"given":"Divyesh","family":"Unadkat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R","family":"Venkatesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"25_CR1","unstructured":"TCS Research. http:\/\/www.tcs.com\/research\/Pages\/default.aspx"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: Verification by Abstraction and Test Generation. In: ASE. pp. 1138\u20131141 (2019)","DOI":"10.1109\/ASE.2019.00121"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: On the glucose sat solver. IJAIT 27(01) (2018)","DOI":"10.1142\/S0218213018400018"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Bardin, A., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATVA. pp. 474\u2013488 (2005)","DOI":"10.1007\/11562948_35"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction withcontinuously-refined invariants. In: CAV. pp. 622\u2013640 (2015)","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programsby tiling. In: SAS. pp. 428\u2013449 (2017)","DOI":"10.1007\/978-3-319-66706-5_21"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programswith full-program induction. In: TACAS (2020)","DOI":"10.1007\/978-3-030-45190-5_2"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In:TACAS (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Darke, P., Prabhu, S., Chimdyalwar, B., Chauhan, A., Kumar, S., Basakchowdhury,A., Venkatesh, R., Datar, A., Medicherla, R.K.: VeriAbs: Verification byAbstraction and Test Generation - (Competition Contribution). In: TACAS. pp.457\u2013462 (2018)","DOI":"10.1007\/978-3-319-89963-3_32"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: TACAS. pp.337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"25_CR11","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.: Ultimateautomizer and the search for perfect interpolants - (competitioncontribution). In: TACAS. pp. 447\u2013451 (2018)","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration ofgeneral linear loops. SIGPLAN Not. 49(1), 529\u2013540 (2014)","DOI":"10.1145\/2578855.2535843"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Khare, S., Saraswat, S., Kumar, S.: Static program analysis of large embeddedcode base: an experience. In: ISEC. pp. 99\u2013102 (2011)","DOI":"10.1145\/1953355.1953368"},{"key":"25_CR14","unstructured":"Kumar, S.: Scaling up Property Checking.https:\/\/www.cse.iitb.ac.in\/~as\/thesis_soft.pdf (2019)"},{"key":"25_CR15","unstructured":"Lattner, C.: LLVM and Clang: Next generation compiler technology. In: The BSDConference (2008)"},{"key":"25_CR16","unstructured":"Zalewski, M.: American fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:08:37Z","timestamp":1616436517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","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":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","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":"40","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":"8","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":"26% - 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":"14","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 conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}