{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:46Z","timestamp":1776305386079,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>VeriAbs is a strategy selection-based reachability verifier for C programs. The selection of a suitable strategy is from a pre-defined set of strategies and by taking into account the syntax and semantics of the code to be verified. This year we present VeriAbs version 1.4.1 in which a novel preprocessor to strategy selection is introduced. The preprocessor checks for the feasibility of performing a lightweight slicing of the input code using function call graph and variable reference information. By this if the program is found to be<jats:italic>sliceable<\/jats:italic>, sub-programs or slices are generated, and the known strategy selection algorithm of VeriAbs is applied to each slice. The verification results of each slice are then composed to derive that of the entire program. This compositional verification has improved the scalability of VeriAbs and presented in this paper.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_32","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"458-462","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6104-9033","authenticated-orcid":false,"given":"Priyanka","family":"Darke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sakshi","family":"Agrawal","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":[[2021,3,23]]},"reference":[{"key":"32_CR1","unstructured":"Foundations of Computing Group at TCS Research. https:\/\/www.tcs.com\/designing-complex-intelligent-systems."},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"M.\u00a0Afzal, A.\u00a0Asia, A.\u00a0Chauhan, B.\u00a0Chimdyalwar, P.\u00a0Darke, A.\u00a0Datar, S.\u00a0Kumar, and R\u00a0Venkatesh. VeriAbs: Verification by Abstraction and Test Generation. In ASE, pages 1138\u20131141, 2019.","DOI":"10.1109\/ASE.2019.00121"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"M.\u00a0Afzal, S.\u00a0Chakraborty, A.\u00a0Chauhan, B.\u00a0Chimdyalwar, P.\u00a0Darke, A.\u00a0Gupta,S.\u00a0Kumar, C.\u00a0Babu M, D.\u00a0Unadkat, and R.\u00a0Venkatesh. Veriabs : Verification by abstraction and test generation (competition contribution). In TACAS\u00a0(2), pages 383\u2013387, 2020.","DOI":"10.1007\/978-3-030-45237-7_25"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"G.\u00a0Audemard and L.\u00a0Simon. On the glucose sat solver. IJAIT, 27(01), 2018.","DOI":"10.1142\/S0218213018400018"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"D.\u00a0Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). In Proc. TACAS\u00a0(2), LNCS\u00a012652. Springer, 2021.","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"D.\u00a0Beyer, M.\u00a0Dangl, and P.\u00a0Wendler. Boosting k-induction with continuously-refined invariants. In CAV, pages 622\u2013640, 2015.","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"S.\u00a0Chakraborty, A.\u00a0Gupta, and D.\u00a0Unadkat. Verifying array manipulating programs with full-program induction. In Proc. TACAS\u00a0(1), pages 22\u201339, 2020.","DOI":"10.1007\/978-3-030-45190-5_2"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"B.\u00a0Chimdyalwar, P.\u00a0Darke, A.\u00a0Chavda, S.\u00a0Vaghani, and A.\u00a0Chauhan. Eliminating static analysis false positives using loop abstraction and bounded model checking. In FM, pages 573\u2013576, 2015.","DOI":"10.1007\/978-3-319-19249-9_35"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"E.\u00a0Clarke, D.\u00a0Kroening, and F.\u00a0Lerda. A Tool for Checking ANSI-C Programs. In TACAS, pages 168\u2013176, 2004.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Mark Harman and Robert\u00a0M. Hierons. An overview of program slicing. Software Focus, 2(3):85\u201392, 2001.","DOI":"10.1002\/swf.41"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"M.\u00a0Heizmann, Y.\u00a0Chen, D.\u00a0Dietsch, M.\u00a0Greitschus, J.\u00a0Hoenicke, Y.\u00a0Li, A.\u00a0Nutz,B.\u00a0Musa, C.\u00a0Schilling, T.\u00a0Schindler, and A.\u00a0Podelski. Ultimate automizer and the search for perfect interpolants - (competition contribution). In TACAS\u00a0(2), pages 447\u2013451, 2018.","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"S.\u00a0Khare, S.\u00a0Saraswat, and S.\u00a0Kumar. Static program analysis of large embedded code base: an experience. In ISEC, pages 99\u2013102, 2011.","DOI":"10.1145\/1953355.1953368"},{"key":"32_CR13","unstructured":"M.\u00a0Zalewski. 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-72013-1_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:45:24Z","timestamp":1671684324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_32","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":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"141","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":"41","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":"21","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":"29% - 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":"12","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 changed to an online format due to the COVID-19 pandemic","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)"}}]}}