{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T06:45:32Z","timestamp":1743835532524,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131844"},{"type":"electronic","value":"9783031131851"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"Abstract<\/jats:title>Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite such a long history, BMC still faces scalability challenges as programs continue to grow larger and more complex. One approach that has proven to be effective in verifying large programs is called Counterexample Guided Abstraction Refinement (CEGAR). In this work, we propose a complementary approach to CEGAR for bounded model checking of sequential programs: in contrast to CEGAR, our algorithm gradually widens underapproximations of a program, guided by the proofs of unsatisfiability. We implemented our ideas in a tool called Legion<\/jats:sc>. We compare the performance of Legion<\/jats:sc> against that of Corral<\/jats:sc>, a state-of-the-art verifier from Microsoft, that utilizes the CEGAR strategy. We conduct our experiments on 727 Windows and Linux device driver benchmarks. We find that Legion<\/jats:sc> is able to solve 12% more instances than Corral<\/jats:sc> and that Legion<\/jats:sc> exhibits a complementary behavior to that of Corral<\/jats:sc>. Motivated by this, we also build a portfolio verifier, $$\\textsc {Legion}^{+}$$<\/jats:tex-math>\n \n L<\/mml:mi>\n \n \n E<\/mml:mi>\n G<\/mml:mi>\n I<\/mml:mi>\n O<\/mml:mi>\n N<\/mml:mi>\n <\/mml:mstyle>\n +<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, that attempts to draw the best of Legion<\/jats:sc> and Corral<\/jats:sc>. Our portfolio, $$\\textsc {Legion}^{+}$$<\/jats:tex-math>\n \n L<\/mml:mi>\n \n \n E<\/mml:mi>\n G<\/mml:mi>\n I<\/mml:mi>\n O<\/mml:mi>\n N<\/mml:mi>\n <\/mml:mstyle>\n +<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, solves 15% more benchmarks than Corral<\/jats:sc> with similar computational resource constraints (i.e. each verifier in the portfolio is run with a time budget that is half of the time budget of Corral<\/jats:sc>). Moreover, it is found to be $$2.9\\times $$<\/jats:tex-math>\n \n 2.9<\/mml:mn>\n \u00d7<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> faster than Corral<\/jats:sc> on benchmarks that are solved by both Corral<\/jats:sc> and $$\\textsc {Legion}^{+}$$<\/jats:tex-math>\n \n L<\/mml:mi>\n \n \n E<\/mml:mi>\n G<\/mml:mi>\n I<\/mml:mi>\n O<\/mml:mi>\n N<\/mml:mi>\n <\/mml:mstyle>\n +<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_15","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"304-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Proof-Guided Underapproximation Widening for\u00a0Bounded Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3320-9543","authenticated-orcid":false,"given":"Prantik","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Jaydeepsinh","family":"Meda","sequence":"additional","affiliation":[]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-023X","authenticated-orcid":false,"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction-and interpolation-based software verification. In: CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alt, L., et al.: Hifrog: Smt-based function summarization for software verification. In: TACAS (2017)","DOI":"10.1007\/978-3-662-54580-5_12"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: FMCAD (2004)","DOI":"10.1007\/978-3-540-30494-4_19"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and static driver verifier: Technology transfer of formal methods inside microsoft. In: International Conference on Integrated Formal Methods (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"15_CR5","unstructured":"Ball, T., Larus, J.R.: Efficient path profiling. In: Proceedings of the 29th Annual ACM\/IEEE International Symposium on Microarchitecture (1996)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bavishi, R., Pandey, A., Roy, S.: To be precise: regression aware debugging. ACM SIGPLAN Notices (2016)","DOI":"10.1145\/2983990.2984014"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, 6\u201311 April, 2019, Proceedings, Part III (2019)","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"15_CR8","unstructured":"Boogie: An intermediate verification language. https:\/\/boogie-docs.readthedocs.io\/en\/latest\/. Accessed June 2022"},{"key":"15_CR9","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: TACAS (2007)"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, P., Chatterjee, A., Campos, J., Abreu, R., Roy, S.: Diagnosing software faults using multiverse analysis. In: IJCAI (2020). https:\/\/doi.org\/10.24963\/ijcai.2020\/226","DOI":"10.24963\/ijcai.2020\/226"},{"key":"15_CR11","unstructured":"Chatterjee, P., Roy, S., Diep, B.P., Lal, A.: Distributed bounded model checking. In: FMCAD (2020)"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, P., Roy, S., Diep, B.P., Lal, A.: Distributed bounded model checking. Formal Methods in System Design (2022). https:\/\/doi.org\/10.1007\/s10703-021-00385-1","DOI":"10.1007\/s10703-021-00385-1"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Chouhan, R., Roy, S., Baswana, S.: Pertinent path profiling: tracking interactions among relevant statements. In: CGO (2013). https:\/\/doi.org\/10.1109\/CGO.2013.6494983","DOI":"10.1109\/CGO.2013.6494983"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV (2000)","DOI":"10.1007\/10722167_15"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: TACAS (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Golia, P., Roy, S., Meel, K.S.: Manthan: a data-driven approach for boolean function synthesis. In: CAV (2020)","DOI":"10.1007\/978-3-030-53291-8_31"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Golia, P., Roy, S., Slivovsky, F., Meel, K.S.: Engineering an efficient boolean functional synthesis engine. In: ICCAD (2021)","DOI":"10.1109\/ICCAD51958.2021.9643583"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL (2005)","DOI":"10.1145\/1040305.1040316"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Notices (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Kroening, D., Tautschnig, M.: Cbmc-c bounded model checker. In: TACAS (2014)","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Roy, S.: Almost correct invariants: synthesizing inductive invariants by fuzzing proofs. In: ISSTA (2022)","DOI":"10.1145\/3533767.3534381"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Reachability modulo theories. In: Reachability Problems - 7th International Workshop, RP (2013)","DOI":"10.1007\/978-3-642-41036-9_4"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using Corral. In: FSE (2014)","DOI":"10.1145\/2635868.2635894"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. ACM SIGPLAN Notices (2015)","DOI":"10.1145\/2737924.2737987"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV (2006)","DOI":"10.1007\/11817963_14"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: TACAS (2003)","DOI":"10.1007\/3-540-36577-X_2"},{"key":"15_CR31","unstructured":"Microsoft: Static Driver Verifier Benchmarks. https:\/\/github.com\/boogie-org\/sdvbench"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Modi, V., Roy, S., Aggarwal, S.K.: Exploring program phases for statistical bug localization. In: PASTE (2013). https:\/\/doi.org\/10.1145\/2462029.2462034","DOI":"10.1145\/2462029.2462034"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: Esbmc 1.22. In: TACAS (2014)","DOI":"10.1007\/978-3-642-54862-8_31"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Pandey, A., Kotcharlakota, P.R.G., Roy, S.: Deferred concretization in symbolic execution via fuzzing. In: ISSTA (2019). https:\/\/doi.org\/10.1145\/3293882.3330554","DOI":"10.1145\/3293882.3330554"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Prabhu, S., Schrammel, P., Srivas, M., Tautschnig, M., Yeolekar, A.: Concurrent program verification with invariant-guided underapproximation. In: ATVA (2017)","DOI":"10.1007\/978-3-319-68167-2_17"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Roy, S.: From concrete examples to heap manipulating programs. In: SAS (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_9","DOI":"10.1007\/978-3-642-38856-9_9"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Roy, S., Srikant, Y.N.: Profiling k-iteration paths: A generalization of the ball-larus profiling algorithm. In: CGO (2009). https:\/\/doi.org\/10.1109\/CGO.2009.11","DOI":"10.1109\/CGO.2009.11"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Verma, A., Kalita, P.K., Pandey, A., Roy, S.: Interactive debugging of concurrent programs under relaxed memory models. In: CGO (2020)","DOI":"10.1145\/3368826.3377910"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Verma, S., Roy, S.: Synergistic debug-repair of heap manipulations. In: ESEC\/FSE (2017)","DOI":"10.1145\/3106237.3106263"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:13:54Z","timestamp":1667495634000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","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":"209","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}