Bubaak: Runtime Monitoring of Program Verifiers

This artifact contains the tool Bubaak in the version used for SV-COMP 2023. Link to the archive on competition's repo: https://gitlab.com/sosy-lab/sv-comp/archives-2023/-/raw/main/2023/bubaak.zip Paper abstract: Bubaak is a program analysis tool that runs analysis algorithms in parallel and uses ideas from runtime monitoring and enforcement to observe and control their progress. In particular, the analysis algorithms send information about (un)reachable states, explored parts of the program, and discovered invariants to a monitor. The monitor can in turn force some of the analyses to stop the search of some parts of the program (which have already been analyzed by other analyses) or make an analysis assume a program invariant found by another analysis. The main analyses used in SV-COMP 2023 are symbolic execution and backward symbolic execution with loop folding. This paper describes both, the design of Bubaak and its implementation participating in SV-COMP 2023, which is still work-in-progress and implements just a subset of the described features