Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking

Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, and Vijay Ganesh

This work is accepted at CAV 2025. A preprint of this article is available for you to download.

Abstract

In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm-selection techniques to select the right tool for a given instance. To automate this process, we present Btor2-Select, a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language Btor2. The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector. Btor2-Select also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive Btor2 benchmark suite coupled with a set of state-of-the-art model checkers, Btor2-Select trained an algorithm selector that successfully closed over 65 % of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary verification engines in parallel. Btor2-Select offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure, Btor2-Select can be easily integrated with new tools and applied to various application domains.

Reproduction Information

A reproduction package of this work is available on Zenodo (DOI). A previous version of the package was reviewed by the Artifact Evaluation Committee of CAV 2025, and awarded the Available and Reusable badges. The updated version incorporates feedbacks from the reviewers and includes additional experiments. The source code and pre-trained models of Btor2-Select is available on GitLab, and the dataset used for training and testing is hosted in a separate repository.

  

Experimental Results

TODO: Add the experimental results here.