Journal of East China Normal University(Natural Science) >
Machine-learning-based model checker performance prediction
Received date: 2023-07-22
Online published: 2024-08-14
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.
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
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. |
/
〈 |
|
〉 |