Theory And Method Of Concurrent Program Verification Based On Interpolation And Partial-order Reduction

With the development of computer technology,software has been integrated into many fields such as mobile communication,rail transportation and financial service.In recent years,however,the faults such as abnormal service access and system crashes caused by software defects occur frequently,some defects even caused immeasurable losses.Hence,it is of great significance to investigate the approaches and techniques that can effectively locate the software defects,improving the reliability and security of software.Program verification is an effective way to improve software quality.It has received extensive attention in the fields of software engineering and system security.As one of the widely used verification approaches,model checking constructs the program model and systematically traverses the corresponding finite state-space to determine whether the program satisfies a given property.However,the exhaustive search often makes model checking methods confront with the state-space explosion problem,making it difficult for programs to be effectively verified within limited resources.For concurrent programs where multiple threads can be executed alternately,the corresponding state-spaces are much larger.Therefore,it is more difficult to verify concurrent programs by utilizing the model checking based approaches.How to effectively deal with the state-space explosion problem of concurrent program verification has been a hot-spot topic in the field of software engineering.This thesis is oriented toward the challenging task of verifying concurrent programs.We first review the general verification theories and methods,and then focus on two kinds of search space reduction techniques(i.e.,interpolation and partial-order reduction):(1)When performing the reachability analysis,some existing interpolation techniques(e.g.,reachability interpolant,universal safety interpolant and existential error interpolant)compute predicates that can be used to prune infeasible branches only when the counterexample-guided abstraction refinement method finds spurious counterexamples.For concurrent programs that are more prone to infeasible branches,such interpolation method fails to improve program analysis precision rapidly,resulting in low verification efficiency.(2)In order to ensure the correctness and completeness of the verification algorithm,most partial-order reduction techniques usually adopt a conservative independence estimation strategy to compute the independence between thread transitions,which makes the partition of trace equivalence classes too detailed.The number of equivalent trace classes to be explored may increase significantly.This thesis revolves around the shortages of the above techniques and aims to improve their effectiveness and practicability in concurrent program verification.We propose the verification theories and approaches that can effectively alleviate the state/trace space explosion problem,and implement an extensible program verification tool,namely PIChecker,based on the configurable program analysis framework CPAchecker.The main contributions and innovations of this thesis are as follows:(1)For the problem that some existing interpolation techniques are difficult to improve the verification efficiency of concurrent programs,we propose a new application of Craig interpolation,namely conditional interpolation.The conditional predicates generated by this technique are mainly used to prune the infeasible conditional branches that occur more frequently due to the alternate execution of threads in concurrent programs.The conditional predicates can be generated before spurious counterexamples are found.Therefore,a large number of conditional predicates can be obtained through multiple different paths in each round of abstraction-refinement iteration,which effectively avoids the problem that only a few number of predicates can be generated from a false path when using the existing interpolation techniques.Meanwhile,a simplification strategy for interpolation paths is proposed,which can significantly improve the efficiency of conditional interpolation.Experimental results show that compared with other interpolation techniques,the proposed conditional interpolation technique increases the number of programs that could be verified by 17.26%,and the number of explored states decreases by 70.13% on average.(2)For the problem that the use of partial-order reduction algorithm based on coarse dependency estimation will lead to redundant exploration,a dynamic partial-order reduction method based on constrained dependency analysis is proposed.This method utilizes the characteristic that isolated transition independent of the transitions of other threads,and performs the prioritized exploration strategy for isolated transition.Meanwhile,this method further uses the dependency constraints in constrained dependency graph to more accurately compute the dependencies between different thread transitions.The combination of prioritized exploration strategy and precise dependency analysis can effectively alleviate the tracespace explosion problem in concurrent program verification.Experimental results show that compared with other partial-order reduction techniques using coarse dependency estimation(e.g.,PPOR and MPOR),the proposed approach can reduce the number of explored states by more than 85.43% on average,shorten the average state-space exploration time by 79.61%,and reduce the average memory cost by 64.96%.(3)We have implemented an extensible program analysis and verification tool based on CPAchecker.PIChecker extends the program analysis method based on the CPA concept and extends the program verification approach by composing multiple program analysis methods and algorithms.Further,this tool combines different program verification approaches,which forms a complete analysis and verification process for concurrent program.It takes advantages of the proposed approaches and increase the number of concurrent programs that can be verified.The experimental results show that PIChecker can verify more programs in limited resources than using different verification approaches alone.In summary,we propose a set of novel theories and reduction approaches for the state-space explosion problem that is more serious in concurrent program verification tasks.We have paved an effective way to improve software reliability and security.