Research On Multicore Bounded Model Checking Technique Based On Interpolation

In the trend of AI,the scale and complexity of information systems are increasing,and people have higher requirements for security and reliability of the systems.As an important automated verification technique,bounded model checking plays an important role in ensuring credibility of the system.By combining bounded model checking and interpolation sequence,the verification of the properties out of some certain boundary can be completed.However,the introduction of interpolation sequence increases the complexity of the model encoding and then affects the overall performance of a model checker.In order to alleviate the problem,the paper proposes interpolation-based multicore bounded model checking method.The main work and innovations of this paper are as follows:Firstly,decomposing large problems into small ones,multicore parallel solutions can effectively shorten the elapsed time of problem processing.According to the conditional predicates,the paths in the model are divided into path clusters,and the interpolation sequence is used to determine if there is no counterexample path in each path cluster.Secondly,based on the nature of fixpoint in the path cluster,we propose a path cluster pruning algorithm in order to reduce the scale of the state space to be searched,which contributes to improving the efficiency.Thirdly,in this paper,we also present two optimization methods: incremental encoding and verification hypothesis.The incremental encoding is to incrementally increase the bound and reduce the number of calls to the solver.The verification hypothesis is mainly to make the most of the verification history information in model checking,and add the verified properties to the propositional formula to improve the efficiency of the interpolation computation.The interpolation-based bounded model checking technique is introduced in the verification of the Hierarchical State Transition Matrix(HSTM)model design,which improves the credibility of the verification results.For the multicore bounded model checking based on interpolation,a series of experiments were carried out on the HSTM model designs from practical projects,and the experimental results are analyzed to validate the effectiveness and efficiency of the method.