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

doi:10.3969/j.issn.1000-5641.2024.04.002

华东师范大学学报（自然科学版） ›› 2024, Vol. 2024 ›› Issue (4): 18-29.doi: 10.3969/j.issn.1000-5641.2024.04.002

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

张枨宇¹(), 诸嘉逸², 黄怿豪³, 杨迪², 李建文², 缪炜恺², 阎迪⁴, 顾斌⁵, 詹乃军⁶, 蒲戈光^2,*()

1. 苏黎世联邦理工学院计算机科学学院, 苏黎世　8006
2. 华东师范大学软件工程学院, 上海　200062
3. 南洋理工大学计算机科学与技术学院, 新加坡　211106
4. 中航商用航空发动机有限责任公司, 上海　200241
5. 中国航天科技集团有限公司, 北京　100048
6. 中国科学院软件研究所, 北京　100190

收稿日期:2023-07-22 出版日期:2024-07-25 发布日期:2024-08-14
通讯作者: 蒲戈光 E-mail:chengyu.zhang@inf.ethz.ch;ggpu@sei.ecnu.edu.cn
作者简介:张枨宇, 男, 博士后, 研究方向为软件工程、形式化方法. E-mail: chengyu.zhang@inf.ethz.ch

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^2,*()

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:2023-07-22 Online:2024-07-25 Published:2024-08-14
Contact: Geguang PU E-mail:chengyu.zhang@inf.ethz.ch;ggpu@sei.ecnu.edu.cn

摘要/Abstract

摘要：

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

关键词: 模型检查, 与非图, 组合模型检查器

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

中图分类号:

TP311

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

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.

图/表 7

图1

图2

图3

图4

表1

图5

图6

参考文献 34

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.

模型	准确度/%		${\Delta _{\rm{avg}}/{\rm{s}} }$
模型	top-1	top-2	top-1	top-2
0-深度编码	0.54	0.83	87.07	13.42
1-深度编码	0.55	0.84	78.89	15.70
2-深度编码	0.55	0.83	65.59	11.24
随机策略	0.26	0.52	450.67	108.98

[1]	陈杰, 沈文怡, 吴问宇, 毛嘉莉. 面向骑行地图推断的轨迹数据质量提升方法[J]. 华东师范大学学报（自然科学版）, 2023, 2023(6): 14-27.
[2]	武朝阳, 毛嘉莉. 基于神经网络的行驶时长预测[J]. 华东师范大学学报（自然科学版）, 2023, 2023(2): 106-118.
[3]	郁毅明, 洪语晨, 王晔, 董启文. 化工材料配方的实验数据治理模块设计[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 1-13.
[4]	李继玲, 李宝林, 严宋如. 疫情背景下快递物流服务的用户行为画像及主题挖掘研究[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 100-114.
[5]	潘晓, 鹿冬娜, 王书海. 基于订单拆分的容量限制商超配送路径规划[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 147-164.
[6]	苗晓变, 廖家俊, 梅华杰, 冯冲, 毛嘉莉. 基于自注意力机制的钢铁物流运力预测[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 165-183.
[7]	邹韬, 钱荣涛, 毛嘉莉. 基于钢铁物流数据的索引与查询技术研究[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 195-207.
[8]	孙晴, 梁冠宇, 武延军, 武斌, 田春岐, 王伟. 数据驱动的开源软件供应链可维护性风险分析方法[J]. 华东师范大学学报（自然科学版）, 2022, 2022(5): 90-99.
[9]	龚鑫, 徐立华, 窦亮, 赵瑞祥. 金融科技软件自动化测试用例的冗余评价和削减方法[J]. 华东师范大学学报（自然科学版）, 2022, 2022(4): 43-55.
[10]	于萍, 胡卉芪, 钱卫宁. 基于遗传算法的多目标货物配载研究[J]. 华东师范大学学报（自然科学版）, 2021, 2021(5): 185-198.
[11]	马晓琴, 郭小鹤, 薛峪峰, 杨琳, 陈远哲. 针对命名实体识别的数据增强技术[J]. 华东师范大学学报（自然科学版）, 2021, 2021(5): 14-23.
[12]	纪宇, 何一璇, 吴国群, 吴敏. 基于Prony-like方法的第一类贝塞尔函数逼近[J]. 华东师范大学学报(自然科学版), 2019, 2019(6): 42-60.
[13]	谢青成, 毛嘉莉, 刘婷. 城市共享单车的动态调度策略[J]. 华东师范大学学报(自然科学版), 2019, 2019(6): 88-102.
[14]	申航杰, 琚生根, 孙界平. 基于模糊聚类和支持向量回归的成绩预测[J]. 华东师范大学学报(自然科学版), 2019, 2019(5): 66-73,84.
[15]	江群, 戴戈南, 张森, 葛又铭, 刘玉葆. 基于用户偏好的最优路径搜索[J]. 华东师范大学学报(自然科学版), 2019, 2019(5): 100-112.

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

Machine-learning-based model checker performance prediction

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 34

相关文章 15

编辑推荐

Metrics

本文评价