{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:59Z","timestamp":1784200259192,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1942537"],"award-info":[{"award-number":["1942537"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by a compositional, summary-based static analysis. The summaries produced by static analysis are used both to prune away infeasible paths and to drive test generation to reach new, unexplored program states. GPS can find both proofs of safety and counter-examples to safety (i.e., inputs that trigger bugs), and features a novel two-layered search strategy that renders it particularly efficient at finding bugs in programs featuring long, input-dependent error paths. To make GPS refutationally complete (in the sense that it will find an error if one exists, if it is allotted enough time), we introduce an instrumentation technique and show that it helps GPS achieve refutation-completeness without sacrificing overall performance. We benchmarked GPS on a diverse suite of benchmarks including programs from the Software Verification Competition (SV-COMP), from prior literature, as well as synthetic programs based on examples in this paper. We found that our implementation of GPS outperforms state-of-the-art software model checkers (including the top performers in SV-COMP ReachSafety-Loops category), both in terms of the number of benchmarks solved and in terms of running time.<\/jats:p>","DOI":"10.1145\/3763142","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2568-2595","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Software Model Checking via Summary-Guided Search"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5348-5468","authenticated-orcid":false,"given":"Ruijie","family":"Fang","sequence":"first","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7294-9165","authenticated-orcid":false,"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Mohammad Afzal A. Asia Avriti Chauhan Bharti Chimdyalwar Priyanka Darke Advaita Datar Shrawan Kumar and R. Venkatesh. 2019. VeriAbs: Verification by Abstraction and Test Generation. In 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 1138-1141. https:\/\/doi.org\/10.1109\/ASE.2019.00121 10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Dirk Beyer Alessandro Cimatti Alberto Griggio M. Erkan Keremoglu Simon Fraser University and Roberto Sebastiani. 2009. Software model checking via large-block encoding. In 2009 Formal Methods in Computer-Aided Design. 25-32. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351147 10.1109\/FMCAD.2009.5351147","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_1_9_2","unstructured":"Dirk Beyer M. Erkan Keremoglu and Philipp Wendler. 2010. Predicate abstraction with adjustable-block encoding. In Formal Methods in Computer Aided Design. 189-197."},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134020"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243849"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632867"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106307"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Ruijie Fang Zachary Kincaid and Thomas Reps. 2025. Artifact for\u201dSoftware Model Checking via Summary-Guided Search\u201d https:\/\/doi.org\/10.5281\/zenodo.16914159 10.5281\/zenodo.16914159","DOI":"10.5281\/zenodo.16914159"},{"key":"e_1_3_1_20_2","unstructured":"Ruijie Fang Zachary Kincaid and Thomas Reps. 2025. Software Model Checking via Summary-Guided Search (Extended Version). arXiv:2508.15137 [cs.PL] https:\/\/arxiv.org\/pdf\/2508.15137"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional recurrence analysis. In 2015 Formal Methods in Computer-Aided Design (FMCAD). 57-64. https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253 10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Arie Gurfinkel and Alexander Ivrii. 2017. K-Induction Without Unrolling. In Formal Methods in Computer-Aided Design (FMCAD).IEEE 1-9. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102243 10.23919\/FMCAD.2017.8102243","DOI":"10.23919\/FMCAD.2017.8102243"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Heqing Huang Yiyuan Guo Qingkai Shi Peisen Yao Rongxin Wu and Charles Zhang. 2022. BEACON: Directed Grey-Box Fuzzing with Provable Path Pruning. In 2022 IEEE Symposium on Security and Privacy (SP). 36-50. https:\/\/doi.org\/10.1109\/SP46214.2022.9833751 10.1109\/SP46214.2022.9833751","DOI":"10.1109\/SP46214.2022.9833751"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_29"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","unstructured":"Dejan Jovanovic and Bruno Dutertre. 2016. Property-Directed k-Induction. In Formal Methods in Computer-Aided Design (FMCAD). IEEE 85-92. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886671 10.1109\/FMCAD.2016.7886671","DOI":"10.1109\/FMCAD.2016.7886671"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Jason Breck Ashkan Forouhi Boroujeni and Thomas W. Reps. 2017. Compositional recurrence analysis revisited. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2017 Barcelona Spain June 18-23 2017. 248-262. https:\/\/doi.org\/10.1145\/3062341.3062373 10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_11"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Rupak Majumdar and Koushik Sen. 2007. Hybrid Concolic Testing. In 29th International Conference on Software Engineering (ICSE\u201907). 416-426. https:\/\/doi.org\/10.1109\/ICSE.2007.41 10.1109\/ICSE.2007.41","DOI":"10.1109\/ICSE.2007.41"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_14"},{"key":"e_1_3_1_41_2","unstructured":"David Molnar P Godefroid and M Levin. 2008. Automated whitebox fuzz testing. In Network and distributed system security symposium NDSS. 416-426."},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572299"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560648"},{"key":"e_1_3_1_45_2","unstructured":"Mary Sheeran Satnam Singh and Gunnar St\u00e5lmarck. 2002. Checking Safety Properties Using Induction and a SAT-Solver. In Formal Methods in Computer-Aided Design (FMCAD) (LNCS Vol. 2517). Springer 108-125."},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_27"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_21"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763142","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:15:14Z","timestamp":1784196914000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":48,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763142"],"URL":"https:\/\/doi.org\/10.1145\/3763142","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}