华东师范大学学报（自然科学版） >

2024 , Vol. 2024 >Issue 4: 18 - 29

DOI: https://doi.org/10.3969/j.issn.1000-5641.2024.04.002

计算机科学

一种基于机器学习的模型检查算法性能预测方法

  • 张枨宇 ,
  • 诸嘉逸 ,
  • 黄怿豪 ,
  • 杨迪 ,
  • 李建文 ,
  • 缪炜恺 ,
  • 阎迪 ,
  • 顾斌 ,
  • 詹乃军 ,
  • 蒲戈光
展开
  • 1. 苏黎世联邦理工学院 计算机科学学院, 苏黎世　8006
    2. 华东师范大学 软件工程学院, 上海　200062
    3. 南洋理工大学 计算机科学与技术学院, 新加坡　211106
    4. 中航商用航空发动机有限责任公司, 上海　200241
    5. 中国航天科技集团有限公司, 北京　100048
    6. 中国科学院 软件研究所, 北京　100190
张枨宇, 男, 博士后, 研究方向为软件工程、形式化方法. E-mail: chengyu.zhang@inf.ethz.ch

收稿日期: 2023-07-22

  网络出版日期: 2024-08-14

收起

Machine-learning-based model checker performance prediction

  • Chengyu ZHANG ,
  • Jiayi ZHU ,
  • Yihao HUANG ,
  • Di YANG ,
  • Jianwen LI ,
  • Weikai MIAO ,
  • Di YAN ,
  • Bin GU ,
  • Naijun ZHAN ,
  • Geguang PU
Expand
  • 1. Department of Computer Science, ETH Zurich, Zurich 8006, Switzerland
    2. Software Engineering Institute, East China Normal University, Shanghai 200062, China
    3. College of Computer Science and Technology, Nanyang Technological University, Singapore　211106, Singapore
    4. Aero Engine Corporation of China, Shanghai　200241, China
    5. China Aerospace Science and Technology Corporation, Beijing　100048, China
    6. The Institute of Software, Chinese Academy of Sciences, Beijing　100190, China

Received date: 2023-07-22

  Online published: 2024-08-14

Fold

摘要

与非图模型是一种表示电路设计的通用基础形式, 同时也是模型检查器的一种通用输入格式. 介绍了一种基于与非图结构编码的特征提取方法, 并基于该方法实现了一种快速的组合模型检查器Liquid. 所提出的结构编码的核心思想: 首先罗列出与非图中所有可能的子结构, 再将每个子结构出现的次数编码成向量, 该向量即作为与非图的特征向量参与之后的机器学习过程. 由于各种模型检查算法的性能在不同的与非图上参差不齐, Liquid的设计目标是组合多种模型检查算法, 针对不同的与非图使用机器学习模型挑选出合适的算法. 收集了目前所有的模型检查器基准测试集作为实验数据集并进行了实验. 实验结果表明, Liquid在实验数据集上的表现优于所有组合中的独立模型检查算法, 并有着不错的预测准确率. 同时, 还从多个维度分析了Liquid有效的原因.

关键词： 模型检查; 与非图; 组合模型检查器

本文引用格式

张枨宇 , 诸嘉逸 , 黄怿豪 , 杨迪 , 李建文 , 缪炜恺 , 阎迪 , 顾斌 , 詹乃军 , 蒲戈光 . 一种基于机器学习的模型检查算法性能预测方法[J]. 华东师范大学学报（自然科学版）, 2024 , 2024(4) : 18 -29 . DOI: 10.3969/j.issn.1000-5641.2024.04.002

Abstract

An and-inverter graph (AIG) is a representation of electrical circuits typically passed as input into a model checker. In this paper, we propose an AIG structural encoding that we use to extract the features of AIGs and construct a portfolio-based model checker called Liquid. The underlying concept of the proposed structural encoding is the enumeration of all possible AIG substructures, with the frequency of each substructure encoded as a feature vector for use in subsequent machine-learning processes. Because the performance of model-checking algorithms varies across different AIGs, Liquid combines multiple such algorithms and selects the algorithm appropriate for a given AIG via machine learning. In our experiments, Liquid outperformed all state-of-the-art model checkers in the portfolio, achieving a high prediction accuracy. We further studied the effectiveness of Liquid from several perspectives.

Key words： model checking; and-inverter graph; portfolio-based model checker

参考文献

1 林梦香, 吴国仕.. 程序模型检查器综述. 计算机软件及计算机应用, 2009, 36 (4): 12- 15.
2 CLARKE E M, EMERSON E A, SIFAKIS J.. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52 (11): 74- 84.
3 MCMILLAN K L. Interpolation and SAT-based model checking [C]// Computer Aided Verification, CAV 2003. 2003: 1-13.
4 GOEL A, SAKALLAH K. Empirical evaluation of IC3-based model checking techniques on Verilog RTL designs [C]// 2019 Design, Automation & Test in Europe Conference & Exhibition. 2019: 618-621.
5 BRAYTON R, MISHCHENKO A. ABC: An academic industrial-strength verification tool [C]// Proceedings of the 22nd International Conference on Computer Aided Verification. 2010: 24-40.
6 BIRER A, DIJK T V, HELJANKO K. Hardware model checking competition [C]// Proceedings of the 17th Formal Methods in Computer-Aided Design. 2017: 9.
7 CABODI G, PALENA M, PASINI P. Interpolation with guided refinement: Revisiting incrementality in sat-base unbounded model checking [C]// Proceedings of the 14th Formal Methods in Computer-Aided Design. 2014: 43-50.
8 LI J W, DUREJA R, PU G G, et al. SimpleCAR: An efficient bug-finding tool based on approximate reachability [C]// Proceedings of the 30th International Conference on Computer Aided Verification. 2018: 37-44.
9 HUBERMAN B A, LUKOSE R M, HOGG T.. An economics approach to hard computational problems. Science, 1997, 275 (5296): 51- 54.
10 XU L, HUTTER F, HOOS H H, et al. SATzilla: Portfolio-based algorithm selection for SAT [J]. Journal of Artificial Intelligence Research, 2008, 32: 565-606.
11 SAT Competition. The SAT 2007 Competition [R/OL]. [2023-03-04]. http://www.satcompetition.org/2007.
12 CABODI G, NOCCO S, QUER S.. Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods in System Design, 2011, 39 (2): 205- 227.
13 BIRER A. The AIGER and-inverter graph (AIG) format version 20071012 [R]. Linz, Austria: Johannes Kepler University, 2007.
14 HASSAN Z, BRADLEY A R, SOMENZI F. Incremental, inductive CTL model checking [C]// Proceedings of the 22nd International Conference on Computer Aided Verification. 2012: 532-547.
15 BRADLEY A R. SAT-based model checking without unrolling [C]// Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation. 2011: 70-87.
16 RICE J R.. The algorithm selection problem. Advances in Computers, 1976, 15, 65- 118.
17 KOTTHOFF L. Algorithm selection for combinatorial search problems: A survey [C]// Data Mining and Constraint Programming. 2016: 149-190.
18 HUTTER F, BABIC D, HOOS H H, et al. Boosting verification by automatic tuning of decision procedures [C]// Proceedings of the 7th Formal Methods in Computer-Aided Design. 2007: 27-34.
19 BALUNOVIC M, BIELIK P, VECHEV M. Learning to solve SMT [C]// Proceedings of the 32nd Conference on Neural Information Processing Systems. 2018: 10338-10349.
20 SCARSELLI F, GORI M, TSOI A C, et al. The graph neural network model [J]. IEEE Transactions on Neural Networks, 2008, 20(1): 61-80.
21 LI Y J, TARLOW D, BROCKSCHMIDT M, et al. Gated graph sequence neural networks [EB/OL]. (2017-09-22) [2023-06-20]. https://arxiv.org/pdf/1511.05493.pdf.
22 SHUAI B, ZOU Z, WANG B, et al. Gag-recurrent neural networks for scene labeling [C]// Proceedings of the Conference on Computer Vision and Pattern Recognition. 2016: 3620-3629.
23 AMIZADEH S, MATUSEVYCH S, WEIMER M. Learning to solve circuit-SAT: An unsupervised differentiable approach [C]// Proceedings of the 6th International Conference on Learning Representations. 2019: 1-14.
24 BRYANT R E.. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986, 100 (8): 677- 691.
25 BIERE A, CIMATTI A, CLARKE E, et al. Symbolic model checking without BDDs [C]// Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1999: 193-207.
26 EEN N, MISHCHENKO A, BRAYTON R. Efficient implementation of property directed reachability [C]// Proceedings of the 11th Formal Methods in Computer-Aided Design. 2011: 125-134.
27 VIZEL Y, GURFINKEL A. Interpolating property directed reachability [C]// Proceedings of the 26th International Conference on Computer Aided Verification. 2014: 260-276.
28 VIZEL Y, WEISSENBACHER G, MALIK S. Boolean satisfiability solvers and their applications in model checking [C]// Proceedings of the IEEE. 2015: 2021-2035.
29 BREIMAN L. Machine Learning [M]. Cambridge, Massachusetts: Massachusetts Institute of Technology Press, 2021.
30 LECUN Y, BENGIO Y, HINTON G. Deep learning [J]. Nature, 2015, 521(7553): 436-444.
31 PEDREGOSA F, VAROQUAUX G, GRAMFORT A, et al. Scikit-learn: Machine learning in Python [J]. Journal of Machine Learning Research, 2011, 12: 2825-2830.
32 MAATEN L V D, HINTON G. Visualizing data using t-SNE [J]. Journal of Machine Learning Research, 2008(9): 2579-2605.
33 BRUMMAYER R, BIERE A, LONSING F. BTOR: Bit-precise modelling of word-level problems for model checking [C]// Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. 2008: 33-38.
34 NIEMETZ A, PREINER M, WOLF C, et al. Btor2, btormc and boolector 3.0 [C]// Proceedings of the 30th International Conference on Computer Aided Verification. 2018: 587-595.
Options
文章导航

/

〈 〉