conference paper published yes Marek Chalupa author 87e34708-d6c6-11ec-9f5b-9391e7be2463 Cedric Richter author ToHe department TACAS: Tools and Algorithms for the Construction and Analysis of Systems Vigilant Algorithmic Monitoring of Software project BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task. https://research-explorer.ista.ac.at/download/15333/15347/2024_LNCS_Chalupa.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Springer Nature2024Luxembourg City, Luxembourg eng 0302-9743 1611-3349 9783031572555 00128418710002010.1007/978-3-031-57256-2_20 14572353–358 M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358. Chalupa, M., &#38; Richter, C. (2024). Bubaak-SpLit: Split what you cannot verify (Competition contribution). In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 353–358). Luxembourg City, Luxembourg: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-57256-2_20">https://doi.org/10.1007/978-3-031-57256-2_20</a> Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 353–358, doi:<a href="https://doi.org/10.1007/978-3-031-57256-2_20">10.1007/978-3-031-57256-2_20</a>. M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition contribution),” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 353–358. Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition contribution). 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 14572, 353–358. Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:353–358. Springer Nature, 2024. <a href="https://doi.org/10.1007/978-3-031-57256-2_20">https://doi.org/10.1007/978-3-031-57256-2_20</a>. Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:353–358. doi:<a href="https://doi.org/10.1007/978-3-031-57256-2_20">10.1007/978-3-031-57256-2_20</a> 153332024-04-20T18:14:06Z2025-09-04T13:48:25Z