Bayesian optimisation of solver parameters in CBMC
CEUR Workshop Proceedings
MetadataShow full item record
Mangla, C., Holden, S., & Paulson, L. (2020). Bayesian optimisation of solver parameters in CBMC. CEUR Workshop Proceedings, 2854 37-47. https://doi.org/10.17863/CAM.55257
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.
This record's DOI: https://doi.org/10.17863/CAM.55257
This record's URL: https://www.repository.cam.ac.uk/handle/1810/308162
All rights reserved