{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:46Z","timestamp":1776305386074,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The main idea behind <jats:sc>Bubaak<\/jats:sc> is to run multiple program analyses in parallel and use <jats:italic>runtime monitoring<\/jats:italic> and <jats:italic>enforcement<\/jats:italic> to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a <jats:italic>monitor<\/jats:italic>. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.<\/jats:p><jats:p>At <jats:sc>SV-COMP<\/jats:sc> \u00a02023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why <jats:sc>Bubaak<\/jats:sc> only ran several analyses in parallel, without any coordination. Still, <jats:sc>Bubaak<\/jats:sc> won the meta-category <jats:italic>FalsificationOverall<\/jats:italic> and placed very well in several other (sub)-categories of the competition.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_32","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"535-540","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Bubaak: Runtime Monitoring of Program Verifiers"],"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-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"32_CR1","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: RV\u201918, pp. 1\u201333. Springer International Publishing (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS\u00a0(2). LNCS\u00a0, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"32_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and validators of the 12th Intl. Competition on Software Verification (SV-COMP 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627829","DOI":"10.5281\/zenodo.7627829"},{"key":"32_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Software verification with PDR: an implementation of the state of the art. In: TACAS\u201920. LNCS, vol. 12078, pp. 3\u201321. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"32_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: CAV\u201915. LNCS, vol.\u00a09206, pp. 622\u2013640. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"32_CR6","doi-asserted-by":"publisher","unstructured":"Bubaak artifact. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.7468631","DOI":"10.5281\/zenodo.7468631"},{"key":"32_CR7","unstructured":"llvm. https:\/\/llvm.org, accessed 2023-02-17"},{"key":"32_CR8","unstructured":"Bubaak repository. https:\/\/gitlab.com\/mchalupa\/bubaak (2022)"},{"key":"32_CR9","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI\u201908. pp. 209\u2013224. USENIX Association (2008), http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"32_CR10","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Mihalkovi\u010d, V., \u0158echt\u00e1\u010dkov\u00e1, A., Zaoral, L., Strej\u010dek, J.: Symbiotic 9: String analysis and backward symbolic execution with loop folding - (competition contribution). In: TACAS\u201922. LNCS, vol. 13244, pp. 462\u2013467. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_32","DOI":"10.1007\/978-3-030-99527-0_32"},{"key":"32_CR11","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J.: Backward symbolic execution with loop folding. In: SAS\u201921. 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":"32_CR12","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol. 10457, pp. 103\u2013134. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_4","DOI":"10.1007\/978-3-319-75632-5_4"},{"key":"32_CR13","doi-asserted-by":"publisher","unstructured":"Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded symbolic execution for program verification. In: Runtime Verification, pp. 396\u2013411. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_32","DOI":"10.1007\/978-3-642-29860-8_32"},{"key":"32_CR14","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"32_CR15","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS\u201908. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"32_CR16","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: FMCAD\u201900. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"32_CR17","unstructured":"Slowbeast repository. https:\/\/gitlab.com\/mchalupa\/slowbeast (2022)"},{"key":"32_CR18","unstructured":"UBSan, https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html, accessed 2023-02-17"}],"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-30820-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:07:16Z","timestamp":1690974436000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_32"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}