Journal of East China Normal University(Natural Science) >

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

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

Computer Science

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

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

Cite this article

Chengyu ZHANG , Jiayi ZHU , Yihao HUANG , Di YANG , Jianwen LI , Weikai MIAO , Di YAN , Bin GU , Naijun ZHAN , Geguang PU . Machine-learning-based model checker performance prediction[J]. Journal of East China Normal University(Natural Science), 2024 , 2024(4) : 18 -29 . DOI: 10.3969/j.issn.1000-5641.2024.04.002

References

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
Outlines

/

〈 〉