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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

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

摘要

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.