Bubaak

Bubaak is a tool for dynamic coopertive verification through instrumentation and runtime monitoring of the verifiers. It uses a task-based architecture where each step in the verification (including compiling the sources, generating counter-examples, etc.) is run as a task. Tasks can be run in sequence and in parallel and can be spawned dynamically based on the information gathered by running or already finished tasks. Thus, the portfolio scheme is not fixed and can be different for each input program or even between two runs on the same input program.

What inputs are supported?

C and LLVM programs, YAML specification of SV-COMP tasks.

For which programming languages has it support?

Bubaak currently targets C programming language.

What properties can be verified?

Assertions, memory safety, undefined behavior, termination.

What are the tool’s main techniques for the supported (input, property) pairs?

Default setup

Forward symbolic execution for all properties. Additionally, Bubaak uses backward symbolic execution with loop folding for verifying assertions and inductive invariants with progress for termination checking.

Other

Bubaak can automatically download and use tools from SV-COMP and run them in a sequential or parallel portfolio. The techniques used then depend on the used tools.

What external tools are used? (e.g., compilers, SMT solvers)

By default BubaaK-LEE (a fork of KLEE) and SlowBeast (both with Z3) and Clang for compiling the code to LLVM. Bubaak can also automatically download and use any tool participating SV-COMP.

What is the tool’s URL?

https://gitlab.com/mchalupa/bubaak

References

[1] Chalupa, M., Henzinger, T.A. (2023). Bubaak: Runtime Monitoring of Program Verifiers. In: Sankaranarayanan, S., Sharygina, N. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science, vol 13994. Springer, Cham. https://doi.org/10.1007/978-3-031-30820-8_32

[2] Chalupa, M., Richter, C. (2024). BUBAAK-SpLit: Split what you cannot verify (Competition contribution). In: Finkbeiner, B., Kovács, L. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024. Lecture Notes in Computer Science, vol 14572. Springer, Cham. https://doi.org/10.1007/978-3-031-57256-2_20