{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:20:19Z","timestamp":1770240019491,"version":"3.49.0"},"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, 418257054"],"award-info":[{"award-number":["378803395, 418257054"]}],"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                    There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries (block contracts) are computed \u2014 based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (computed from postconditions received from block predecessors, i.e., which program states reach this block) and violation conditions to check at the block exit (computed from violation conditions received from block successors, i.e., which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a postcondition or violation condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach on the basis of configurable program analysis and implement it for the verification of C programs in the widely used verifier\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    . A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well, and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.\n                  <\/jats:p>","DOI":"10.1145\/3660766","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T10:22:09Z","timestamp":1720779729000},"page":"1307-1329","source":"Crossref","is-referenced-by-count":3,"title":["Decomposing Software Verification using Distributed Summary Synthesis"],"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-7365-5030","authenticated-orcid":false,"given":"Matthias","family":"Kettl","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","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-031-57256-2_15"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2949"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_28"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054162"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_1_13_2","unstructured":"T. Ball and S. K. Rajamani. 2000. Boolean programs: A model and process for software analysis. Technical Report MSR Tech. Rep. 2000-14. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/tr-2000-14.pdf."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_1_17_2","first-page":"189","volume-title":"Proc. FMCAD","author":"Beyer D.","year":"2010","unstructured":"D. Beyer, M. E. Keremoglu, and P. Wendler. 2010. Predicate abstraction with adjustable-block encoding. In Proc. FMCAD. FMCAD, 189\u2013197. https:\/\/ieeexplore.ieee.org\/document\/5770949."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_24"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238195"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409718"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"L. Alt S. Asadi H. Chockler K. Even-Mendoza G. Fedyukovich A. E. J. Hyv\u00e4rinen and N. Sharygina. 2017. HiFrog: SMT-based function summarization for software verification. In Proc. TACAS (LNCS 10206). 207\u2013213. https:\/\/doi.org\/10.1007\/978-3-662-54580-5_12 10.1007\/978-3-662-54580-5_12","DOI":"10.1007\/978-3-662-54580-5_12"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.29007\/d3bt"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_1_31_2","first-page":"5","volume-title":"Proc. ILPS","author":"Reps T. W.","year":"1997","unstructured":"T. W. Reps. 1997. Program analysis via graph reachability. In Proc. ILPS. MIT, 5\u201319."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454044"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.275.5296.51"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_27"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_30"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_5"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-019-00331-9"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232423"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2501854"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"e_1_3_1_53_2","volume-title":"Sylvan: Multi-core decision diagrams","author":"van Dijk T.","year":"2016","unstructured":"T. van Dijk. 2016. Sylvan: Multi-core decision diagrams. Ph. D. Dissertation. University of Twente, Enschede, Netherlands. http:\/\/purl.utwente.nl\/publications\/100676"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.13"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_19"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1008.1459"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","unstructured":"D. Beyer N.-Z. Lee and P. Wendler. 2024. Interpolation and SAT-based model checking revisited: Adoption to software verification. J. Autom. Reasoning (2024). https:\/\/doi.org\/10.1007\/s10817-024-09702-9 10.1007\/s10817-024-09702-9 Preprint: https:\/\/doi.org\/10.48550\/arXiv.2208.05046 10.48550\/arXiv.2208.05046.","DOI":"10.1007\/s10817-024-09702-9"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"e_1_3_1_63_2","volume-title":"Proc. FASE (LNCS 13991)","author":"Beyer D.","year":"2023","unstructured":"D. Beyer. 2023. Software testing: 5th comparative evaluation: Test-Comp 2023. In Proc. FASE (LNCS 13991). Springer."},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","unstructured":"D. Beyer M. Kettl and T. Lemberger. 2024. Reproduction package for FSE 2024 article \u2018Decomposing software verification using distributed summary synthesis\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.11563223 10.5281\/zenodo.11563223","DOI":"10.5281\/zenodo.11563223"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/1465482.1465560"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477579"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-020-00270-x"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660766","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3660766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T08:06:24Z","timestamp":1770192384000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660766"}},"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\/3660766"],"URL":"https:\/\/doi.org\/10.1145\/3660766","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}