Bayesian Optimisation of Solver Parameters in CBMC

Satisfiability solvers can be embedded in applications to perform specific formal reasoning tasks. CBMC, for example, is a bounded model checker for C and C++ that embeds SMT and SAT solvers to check internally generated formulae. Such solvers will be solely used to evaluate the class of formulae generated by the embedding application and therefore may benefit from domain-specific parameter tuning. We propose the use of Bayesian optimisation for this purpose, which offers a principled approach to black-box optimisation within limited resources. We demonstrate its use for optimisation of the solver embedded in CBMC specifically for a collection of test harnesses in active industrial use, for which we have achieved a significant improvement over the default parameters.