{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:48Z","timestamp":1776305388266,"version":"3.50.1"},"publisher-location":"Cham","reference-count":9,"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>Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though).<\/jats:p>\n          <jats:p>\n            <jats:sc>Bubaak<\/jats:sc> is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. <jats:sc>Bubaak<\/jats:sc> starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with <jats:sc>Bubaak<\/jats:sc> as an intermediary.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_14","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:17Z","timestamp":1746005897000},"page":"212-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["BUBAAK: Dynamic Cooperative Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1132-5516","authenticated-orcid":false,"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2906-6508","authenticated-orcid":false,"given":"Cedric","family":"Richter","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"14_CR1","unstructured":"Beyer, D., Strej\u010dek, J.: Report on SV-COMP 2025. In: Proc. TACAS. LNCS\u00a0, Springer (2025)"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: On-demand composition of cooperative verification systems. In: Proc. TACAS 2022, Part I. LNCS, vol. 13243, pp. 561\u2013579. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Proc. SEFM 2022. LNCS, vol. 13550, pp. 111\u2013128. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7","DOI":"10.1007\/978-3-031-17108-6_7"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA 2020, Part I. LNCS, vol. 12476, pp. 143\u2013167. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bubaak artifact. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.14205712","DOI":"10.5281\/zenodo.14205712"},{"key":"14_CR6","unstructured":"Bubaak repository. https:\/\/gitlab.com\/mchalupa\/bubaak (2022)"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Henzinger, T.A.: Bubaak: Runtime monitoring of program verifiers - (competition contribution). In: Proc. TACAS 2023, Part II. LNCS, vol. 13994, pp. 535\u2013540. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_32","DOI":"10.1007\/978-3-031-30820-8_32"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J.: Backward symbolic execution with loop folding. In: Proc. SAS 2021. LNCS, vol. 12913, pp. 49\u201376. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_3","DOI":"10.1007\/978-3-030-88806-0_3"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004. pp. 75\u201388. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:19Z","timestamp":1746005899000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_14"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_14","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"}}]}}