Bubaak-SpLit: Split what you cannot verify (Competition contribution)

Abstract

Abstract Bubaak-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top ofBubaak, a tool designed for running combinations of verifiers in parallel. In contrast toBubaak, that directly invokes verifiers on the inputs,Bubaak-SpLit first starts by splitting the input program into multiple modified versions calledprogram splits. During the splitting process,Bubaak-SpLit utilizes aweakverifier (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 ofhard-to-verifyprogram splits is generated or a splitting limit is reached. During the main verification phase, we run a combination ofBubaak-LeeandSlowbeastin parallel on the remaining unsolved parts of the verification task.