{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:18Z","timestamp":1779074478183,"version":"3.51.4"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T00:00:00Z","timestamp":1720742400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["378803395"],"award-info":[{"award-number":["378803395"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2024,7,12]]},"abstract":"<jats:p>\n                    Assuring the correctness of computing systems is fundamental to our society and economy, and\n                    <jats:italic toggle=\"yes\">formal verification<\/jats:italic>\n                    is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades,\n                    <jats:italic toggle=\"yes\">Craig interpolation<\/jats:italic>\n                    has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1)\n                    <jats:italic toggle=\"yes\">Interpolation-Sequence-Based Model Checking<\/jats:italic>\n                    (Vizel and Grumberg, 2009) and (2)\n                    <jats:italic toggle=\"yes\">Intertwined Forward-Backward Reachability Analysis Using Interpolants<\/jats:italic>\n                    (Vizel, Grumberg, and Shoham, 2013), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.\n                  <\/jats:p>","DOI":"10.1145\/3660797","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T10:22:09Z","timestamp":1720779729000},"page":"2028-2050","source":"Crossref","is-referenced-by-count":5,"title":["A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7961-190X","authenticated-orcid":false,"given":"Marek","family":"Jankola","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,12]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113767"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123223"},{"key":"e_1_3_1_5_2","volume-title":"Handbook of Satisfiability","author":"Biere A.","year":"2009","unstructured":"A. Biere, M. Heule, H. van Maaren, and T. Walsh (Eds.). 2009. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press. ISBN: 978-1-58603-929-5"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437479.3437483"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2010.03525"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/IWSM-MENSURA.2013.22"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3241743"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-024-09702-9"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_1_25_2","article-title":"Software verification with CPAchecker 3.0: Tutorial and user guide","author":"Baier D.","year":"2024","unstructured":"D. Baier, D. Beyer, P.-C. Chien, M.-C. Jakobs, M. Jankola, M. Kettl, N.-Z. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, and P. Wendler. 2024. Software verification with CPAchecker 3.0: Tutorial and user guide. In Proc. FM (LNCS). Springer.","journal-title":"Proc. FM (LNCS)"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"D. Beyer. 2023. SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2023 and Test-Comp 2023). Zenodo. https:\/\/doi.org\/10.5281\/zenodo.7627783 10.5281\/zenodo.7627783","DOI":"10.5281\/zenodo.7627783"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1038\/533452a"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pmed.0020124"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2658987"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25231-0_2"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-044-5_14"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2812803"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038650"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549172"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09851-6"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409767"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-09973-5"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_1_41_2","first-page":"209","article-title":"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"Cadar C.","year":"2008","unstructured":"C. Cadar, D. Dunbar, and D.R. Engler. 2008. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. OSDI. USENIX Association, 209\u2013224. https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756","journal-title":"Proc. OSDI"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884835"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_6"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_15"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-019-00547-X"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_22"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.13"},{"key":"e_1_3_1_61_2","author":"Aho A. V.","year":"1986","unstructured":"A. V. Aho, R. Sethi, and J.D. Ullman. 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley. ISBN: 978-0-201-10088-4 https:\/\/www.worldcat.org\/isbn\/978-0-201-10088-4","journal-title":"Compilers: Principles, Techniques, and Tools"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0124-2"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_19"},{"key":"e_1_3_1_66_2","first-page":"51","volume-title":"Proc. FMCAD","author":"Cimatti A.","year":"2010","unstructured":"A. Cimatti, A. Micheli, I. Narasamdya, and M. Roveri. 2010. Verifying SystemC: A software model checking approach. In Proc. FMCAD. FMCAD Inc., 51\u201359. https:\/\/ieeexplore.ieee.org\/document\/5770933"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","unstructured":"D. Beyer P.-C. Chien M. Jankola and N.-Z. Lee. 2024. Reproduction package for FSE 2024 article\u2019A transferability study of interpolation-based hardware model checking for software verification\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.11070973 10.5281\/zenodo.11070973","DOI":"10.5281\/zenodo.11070973"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660797","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3660797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:54:55Z","timestamp":1770191695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,12]]},"references-count":67,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2024,7,12]]}},"alternative-id":["10.1145\/3660797"],"URL":"https:\/\/doi.org\/10.1145\/3660797","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}