Research On System Optimization For Path-Oriented Bounded Model Checking

With the advance of informatization construction,the role of computer science is becoming more and more important in all walks of life.The security issues of software systems have correspondingly received a lot of attention.As a widely-used programming language in key areas such as aerospace,subway transportation,national defense,etc.,the correctness of C programs should always be regarded as essential.Researchers have developed a variety of model checking tools for C programs such as CBMC,CPAChecker.However,the above methods and tools are all for the verification of the overall problem converted from the C programs.As the code size continues to expand,it will cause the space explosion,making the problem scale beyond the support of the underlying solver,and causing great obstacles to the verification process.To this end,in the previous work,we have proposed a path-oriented bounded model checking algorithm called SAT-LP-IIS,which can control the verification complexity to some extent.Based on this,a simple prototype has been implemented.However,when we apply this method to verify the real-world C programs,there are still many challenges.First,there will be a large number of paths to be traversed when processing large-scale code,which can lead to a path explosion problem.So a more efficient path traversal method is required.Second,when the input code contains a loop structure with a large number of iterations,the length of the path can be too long to handle.So we need a method and framework to preprocess the loop effectively.In order to address these issues and apply our method to practical applications,this work has mainly made the following contributions:To deal with the current problem of path explosion,a new path traversal method is proposed.This method is based on parallel computing technology.It speeds up verification by verifying multiple paths in parallel.At the same time,it uses a shared infeasible path pool to simultaneously feed back the verification results of each path to avoid unnecessary calculations,thereby improving the overall verification efficiency.To solve the problem that the loop structure with a large number of iterations cannot be effectively dealt with,this work proposes an integrated preprocessing framework for the loop structure.The framework uses loop summarization technology and loop abstraction technology to preprocess the loop before verification.The system's ability to process the loop structure can thus be improved.Intending to implement our method on the bounded model checking of real-world C programs,and evaluate the effectiveness of our work in this thesis,we developed a bounded model checking tool BRICK for C code based on the optimized algorithm and framework.Besides,we add the overall support of multiple common technologies to BRICK.Experiment results show that BRICK has better performance advantages compared to its previous version and tools of the same kind.