{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:47Z","timestamp":1776305387198,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","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>We present VeriAbsL, a reachability verifier that performs verification in three stages. First, it slices the input code using a combination of two slicers, then it verifies the slices using <jats:italic>predicted<\/jats:italic> strategies, and at last, it composes the result of verifying the individual slices. We introduce a novel <jats:italic>shallow slicing<\/jats:italic> technique that uses variable reference information of the program, and data and control dependencies of the entry function to generate slices. We also introduce a novel <jats:italic>strategy prediction<\/jats:italic> technique that uses machine learning to predict a strategy. It uses boolean features to describe a program to a neural network that predicts a strategy. We use the portfolio of VeriAbs, a reachabiltiy verifier with manually defined strategies. In <jats:sc>sv-comp<\/jats:sc> 2023, VeriAbsL verified 227 (Without witness validation.) more programs than VeriAbs, and 475 (Without witness validation.) programs that VeriAbs could not verify.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_41","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"588-593","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (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":"Bharti","family":"Chimdyalwar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sakshi","family":"Agrawal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shrawan","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R","family":"Venkatesh","sequence":"additional","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"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"41_CR1","unstructured":"Foundations of Computing Group at TCS Research. https:\/\/www.tcs.com\/what-we-do\/research."},{"key":"41_CR2","unstructured":"TensorFlow. https:\/\/www.tensorflow.org\/."},{"key":"41_CR3","unstructured":"VeriAbsL Tool Archive. https:\/\/gitlab.com\/sosy-lab\/sv-comp\/archives-2023\/-\/blob\/main\/2023\/veriabsl.zip."},{"key":"41_CR4","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":"41_CR5","doi-asserted-by":"crossref","unstructured":"Dirk Beyer. Progress on software verification: SV-COMP 2022. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, volume 13244 of Lecture Notes in Computer Science, pages 375\u2013402. Springer, 2022.","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"41_CR6","unstructured":"Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. Verifying array manipulating programs with full-program induction. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 22\u201339. Springer, 2020."},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"P.\u00a0Darke, S.\u00a0Agrawal, and R.\u00a0Venkatesh. VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). In Proc. TACAS\u00a0(2), LNCS\u00a012652. Springer, 2021.","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"41_CR8","unstructured":"Yulia Demyanova, Thomas Pani, Helmut Veith, and Florian Zuleger. Empirical software metrics for benchmarking of verification tools. In Jens Knoop and Uwe Zdun, editors, Software Engineering 2016, pages 67\u201368, Bonn, 2016. Gesellschaft f\u00fcr Informatik e.V."},{"key":"41_CR9","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":"41_CR10","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":"41_CR11","doi-asserted-by":"crossref","unstructured":"Will Leeson and Matthew\u00a0B. Dwyer. Graves-cpa: A graph-attention verifier selector (competition contribution). In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 440\u2013445, Cham, 2022. Springer International Publishing.","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Cedric Richter, Eyke H\u00fcllermeier, Marie-Christine Jakobs, and Heike Wehrheim. Algorithm selection for software validation based on graph kernels, 2020. https:\/\/link.springer.com\/article\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"Cedric Richter and Heike Wehrheim. Pesco: Predicting sequential combinations of verifiers. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 229\u2013233, Cham, 2019. Springer International Publishing.","DOI":"10.1007\/978-3-030-17502-3_19"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:07:55Z","timestamp":1690974475000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_41","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":"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":"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":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","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":"169","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":"56","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":"6","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":"33% - 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":"11","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)"}}]}}