TY - GEN
T1 - A Novel Approach for Bounded Model Checking Through Full Parallelism
AU - Sang, Debao
AU - Liu, Jing
AU - Sun, Haiying
AU - Xu, Jin
AU - Kang, Jiexiang
N1 - Publisher Copyright:
© 2022 IEEE.
PY - 2022
Y1 - 2022
N2 - Bounded Model Checking (BMC) has been found promising in finding deep vulnerabilities in industry designs and scaling well with design sizes. However, the parallelisation of BMC is challenging, due to the propositional satisfiability (SAT) problem and satisfiability modulo theories problem solving being hard to parallelise. In this paper, we propose a novel approach to perform BMC based on the mathematical model of probe machine, which is the first approach to employ probe machine to accelerate BMC, particularly it can solve SAT formulas in full parallel. We introduce the workflow of the algorithm and explain in detail the process of mapping BMC to the probe machine. A method is provided to prove the correctness of the algorithm and to analyze its time complexity. We develop a model checker called BMC2PROBE based on our approach and explain the framework and memory management of the tool. The experiment results are discussed, which prove the feasibility and effectiveness of our approach.
AB - Bounded Model Checking (BMC) has been found promising in finding deep vulnerabilities in industry designs and scaling well with design sizes. However, the parallelisation of BMC is challenging, due to the propositional satisfiability (SAT) problem and satisfiability modulo theories problem solving being hard to parallelise. In this paper, we propose a novel approach to perform BMC based on the mathematical model of probe machine, which is the first approach to employ probe machine to accelerate BMC, particularly it can solve SAT formulas in full parallel. We introduce the workflow of the algorithm and explain in detail the process of mapping BMC to the probe machine. A method is provided to prove the correctness of the algorithm and to analyze its time complexity. We develop a model checker called BMC2PROBE based on our approach and explain the framework and memory management of the tool. The experiment results are discussed, which prove the feasibility and effectiveness of our approach.
KW - bounded model checking
KW - graph search
KW - probe machine
UR - https://www.scopus.com/pages/publications/85151477948
U2 - 10.1109/QRS57517.2022.00046
DO - 10.1109/QRS57517.2022.00046
M3 - 会议稿件
AN - SCOPUS:85151477948
T3 - IEEE International Conference on Software Quality, Reliability and Security, QRS
SP - 376
EP - 387
BT - Proceedings - 2022 IEEE 22nd International Conference on Software Quality, Reliability and Security, QRS 2022
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 22nd IEEE International Conference on Software Quality, Reliability and Security, QRS 2022
Y2 - 5 December 2022 through 9 December 2022
ER -