In recent times, Bounded Model Checking (BMC) engines are gaining wide prominence and showing great effectiveness in formal verification. Today, an arsenal of different BMC engines exist, differing widely in the optimization, representations and solving mechanisms used to represent and navigate the underlying state transition system as they look for property violations. When having a concrete verification task at hand, a designer is often confronted with the problem of engine selection, and more often than not, has to resort to manually designed selection heuristics or machine-learned strategies using carefully selected features of the design. It has often been observed that these different engines have different strengths and weaknesses, depending on the nature of the verification task, the property and the complexity of the design. This talk will present a recent work that was set off to examine if combinations of these engines can help to combine the strengths. We talk about a recent work from our group that proposes an approach to create a sequencing of BMC engines that can reach better depths in formal verification, as opposed to executing them alone. Our approach uses machine learning, specifically, the Multi-Armed Bandit paradigm of Reinforcement Learning, to predict the best-performing BMC engine for a given unrolling depth of the underlying design transition system. We present an evaluation of our approach to show that our proposed approach outperforms state-of-the-art BMC engines in terms of the depth reached or time taken to deduce a property violation on the Hardware Model Checking Competition (HWMCC) benchmarks.
