{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:31Z","timestamp":1776305371037,"version":"3.50.1"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present Nacpa, a meta-verifier based on parallel portfolio and native compilation of backend verifiers. Nacpa does not implement any software analyses itself, but uses the Java-based <jats:sc>CPAchecker<\/jats:sc> as off-the-shelf verification backend in different configurations; each called as a separate, external process. To avoid the overhead of starting the Java Virtual Machine multiple times and to improve the run time on fast-to-solve tasks, we created a natively compiled version of <jats:sc>CPAchecker<\/jats:sc> for Nacpa. Nacpa is a conceptually simple framework, yet proves to be competitive in SV-COMP \u00a02025.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_18","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:40Z","timestamp":1746005860000},"page":"236-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Nacpa: Native Checking with Parallel-Portfolio\u00a0Analyses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4768-4054","authenticated-orcid":false,"given":"Henrik","family":"Wachowitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS\u00a06806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Baier, D., Beyer, D., Chien, P.C., Jankola, M., Kettl, M., Lee, N.Z., Lemberger, T., Lingsch-Rosenfeld, M., Spiessl, M., Wachowitz, H., Wendler, P.: CPAchecker 2.3 with strategy selection (competition contribution). In: Proc. TACAS\u00a0(3). pp. 359\u2013364. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_21","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"18_CR3","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS. LNCS, Springer (2025)"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on boolean features: A simple but effective approach. In: Proc. ISoLA. pp. 144\u2013159. LNCS\u00a011245, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11, https:\/\/www.sosy-lab.org\/research\/pub\/2018-ISoLA.Strategy_Selection_for_Software_Verification_Based_on_Boolean_Features.pdf","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Bentele, M., Dietsch, D., Jiang, X., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS\u00a0(3). pp. 418\u2013423. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_31","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate Taipan 2023 (competition contribution). In: Proc. TACAS\u00a0(2). pp. 582\u2013587. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_40","DOI":"10.1007\/978-3-031-30820-8_40"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Klumpp, D., Dietsch, D., Heizmann, M., Sch\u00fcssele, F., Ebbinghaus, M., Farzan, A., Podelski, A.: Ultimate GemCutter and the axes of generalization (competition contribution). In: Proc. TACAS\u00a0(2). pp. 479\u2013483. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_35","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Leeson, W., Dwyer, M.: Graves-CPA: A graph-attention verifier selector (competition contribution). In: Proc. TACAS\u00a0(2). pp. 440\u2013445. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_28","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lemberger, T., Wachowitz, H.: CPA-Daemon: Mitigating tool restarts for Java-based verifiers. In: Proc. ATVA. Springer (2024)","DOI":"10.1007\/978-3-031-78750-8_8"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Lemberger, T., Wachowitz, H.: Nacpa release 1.0. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.14203473","DOI":"10.5281\/zenodo.14203473"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wachowitz, H.: FM-Weck: Containerized execution of formal-methods tools. In: Proc. FM. LNCS\u00a014934, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_3","DOI":"10.1007\/978-3-031-71177-0_3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:43Z","timestamp":1746005863000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_18"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}