{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:06:27Z","timestamp":1776305187805,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":102,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,21]],"date-time":"2022-05-21T00:00:00Z","timestamp":1653091200000},"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":["418257054"],"award-info":[{"award-number":["418257054"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,21]]},"DOI":"10.1145\/3510003.3510064","type":"proceedings-article","created":{"date-parts":[[2022,7,5]],"date-time":"2022-07-05T22:42:59Z","timestamp":1657060979000},"page":"536-548","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Decomposing software verification into off-the-shelf components"],"prefix":"10.1145","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Haltermann","sequence":"additional","affiliation":[{"name":"University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[{"name":"LMU Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_27"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00121"},{"key":"e_1_3_2_1_3_1","volume-title":"Programming Languages --- C","author":"American National Standards Institute. 1999. ANSI\/ISO\/IEC 9899-1999","unstructured":"American National Standards Institute. 1999. ANSI\/ISO\/IEC 9899-1999: Programming Languages --- C. American National Standards Institute, 1430 Broadway, New York, NY 10018, USA."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71734-0_2"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768820080022"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950349"},{"key":"e_1_3_2_1_7_1","volume-title":"Technical Report MSR-TR-2002-09. Microsoft Research.","author":"Ball T.","year":"2002","unstructured":"T. Ball and S. K. Rajamani. 2002. Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09. Microsoft Research."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9246-5"},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. SMT.","author":"Barrett C.","unstructured":"C. Barrett, A. Stump, and C. Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proc. SMT."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_1_12_1","first-page":"15","article-title":"ACSL","volume":"1","author":"Baudin P.","year":"2020","unstructured":"P. Baudin, P. Cuoq, J.-C. Filli\u00e2tre, C. March\u00e9, B. Monate, Y. Moy, and V. Prevosto. 2020. ACSL: ANSI\/ISO C Specification Language Version 1.15.","journal-title":"ANSI\/ISO C Specification Language Version"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060770"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_2"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950351"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786867"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_26"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5301636"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_4"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.13"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180259"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_9"},{"key":"e_1_3_2_1_33_1","volume-title":"Proc. TACAS. Springer.","author":"Beyer D.","unstructured":"D. Beyer and S. Kanav. 2022. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems (forthcoming). In Proc. TACAS. Springer."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. FMCAD. FMCAD, 189--197","author":"Beyer D.","unstructured":"D. Beyer, M. E. Keremoglu, and P. Wendler. 2010. Predicate Abstraction with Adjustable-Block Encoding. In Proc. FMCAD. FMCAD, 189--197."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_11"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_15"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"e_1_3_2_1_42_1","volume-title":"Impact. In Proc. FMCAD. FMCAD, 106--113","author":"Beyer D.","unstructured":"D. Beyer and P. Wendler. 2012. Algorithms for Software Model Checking: Predicate Abstraction vs. Impact. In Proc. FMCAD. FMCAD, 106--113."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75698-9_2"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/2366366.2366368"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136004"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_27"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115633"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45212-6_9"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2949"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_36"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"e_1_3_2_1_59_1","volume-title":"Specification, Algebra, and Software","author":"Cruanes Simon","unstructured":"Simon Cruanes, Stijn Heymans, Ian Mason, Sam Owre, and Natarajan Shankar. 2014. The Semantics of Datalog for the Evidential Tool Bus. In Specification, Algebra, and Software. Springer, 256--275."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45828-x_9"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5"},{"key":"e_1_3_2_1_64_1","volume-title":"Structured Analysis and System Specification (facsimile ed.)","author":"DeMarco T.","unstructured":"T. DeMarco. 1979. Structured Analysis and System Specification (facsimile ed.). Prentice Hall. ISBN: 978-0138543808"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106307"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_13"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_12"},{"key":"e_1_3_2_1_68_1","volume-title":"Proc. SMT.","author":"Gario M.","unstructured":"M. Gario and A. Micheli. 2015. PySMT: A solver-agnostic library for fast prototyping of SMT-Based algorithms. In Proc. SMT."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","unstructured":"P. Godefroid and K. Sen. 2018. Combining Model Checking and Testing. In Handbook of Model Checking. Springer 613--649. 10.1007\/978-3-319-10575-8_19","DOI":"10.1007\/978-3-319-10575-8_19"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_7"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_6"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081713"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_71"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_24"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v33i1.2395"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_11"},{"key":"e_1_3_2_1_85_1","unstructured":"M. Mann A. Wilson C. Tinelli and C. W. Barrett. 2020. SMT-Switch: A solver-agnostic C++ API for SMT Solving. arXiv\/CoRR 2007.01374 (2020). arXiv:2007.01374 https:\/\/arxiv.org\/abs\/2007.01374."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-004-0072-z"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_38"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2005.59"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338915"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040317"},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-020-00270-x"},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"e_1_3_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_3"},{"key":"e_1_3_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_20"},{"key":"e_1_3_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050003"},{"key":"e_1_3_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2357442"},{"key":"e_1_3_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.15514\/ISPRAS-2017-29(4)-13"},{"key":"e_1_3_2_1_102_1","unstructured":"D. Wang C. Zhang G. Chen M. Gu and J. Sun. 2016. C Code Verification based on the Extended Labeled Transition System Model. In MoDELS 2016 (CEUR 1725). CEUR-WS.org 48--55."},{"key":"e_1_3_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2864122"}],"event":{"name":"ICSE '22: 44th International Conference on Software Engineering","location":"Pittsburgh Pennsylvania","acronym":"ICSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 44th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510003.3510064","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3510003.3510064","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:12:04Z","timestamp":1750191124000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510003.3510064"}},"subtitle":["an application to CEGAR"],"short-title":[],"issued":{"date-parts":[[2022,5,21]]},"references-count":102,"alternative-id":["10.1145\/3510003.3510064","10.1145\/3510003"],"URL":"https:\/\/doi.org\/10.1145\/3510003.3510064","relation":{},"subject":[],"published":{"date-parts":[[2022,5,21]]},"assertion":[{"value":"2022-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}