Research On CEGAR Based Model Checking For C Programs

Software has been an indispensable element in the social development,which is successfully used in many critical areas,such as aerospace,medical,transport.With the increasing importance of software,the reliability and safety of software are naturally focused.For a long time,researchers have been researching how to find the hidden errors in software for assuring the reliability and safety.Model checking is one of the most widely used and very effective approaches.It models a program and formalizes the verified property,which checks automatically whether the program satisfies the verified property.However,state space explosion is a key problem in model checking,which affects the capacity of model checking seriously and reduces the effect in large-scale programs.Hence,how to improve the efficiency and scalability of model checking for better applying to large-scale programs has been a research hotspot.GEGAR(Counterexample-guided Abstraction Refinement)technique can effectively reduce state space to advance the efficiency in model checking.It also has a good effect on large-scale programs.The paper mainly investigates the CEGAR based abstraction model checking algorithm,researches and discusses how to alleviate the state space explosion when automatically verifying the programs.The main contributions and contents in the paper are shown as follows:Firstly,an approach to CEGAR based model checking which has proved to be successful on large models can employ Craig interpolation to efficiently construct predicate abstractions.In order to systematically reduce the program state space to be explored for safety verification,the paper introduces two new kinds of applications,universal safety interpolant and existential error interpolant,of Craig interpolation.Whenever the universal safety interpolant at a location is implied by the current path,all paths emanating from that location are guaranteed to be safe.Dually whenever the existential error interpolant at a location is implied by the current path,there is guaranteed to be an unsafe path from the location,that is,can reach the error state.Meanwhile,the paper proposes two optimization strategies so that new interpolants can be more effectively used.The paper shows how these interpolants are computed and applied in safety verification,and has implemented our approach in a software model checker named INTERPCHECKER.Experiments on a large number of benchmark programs show that both the interpolations and the auxiliary optimization strategies are effective in improving scalability of software model checking.Secondly,to verify both safety and liveness temporal properties of programs in practice,the paper researches the verification approach in safety property,and extends the approach to verify temporal properties.First,aiming at null pointer dereference problem of C programs,the paper uses LTL(Linear Temporal Logic)to describe the problem,and then combines with CFG(Control Flow Graph)to check whether the program satisfies the property.Next,the paper extends the approach to verify the general temporal properties.First,LTL is extended to finite models,and the algorithm for transforming LTL formula to DFA(Deterministic Finite Automata)is proposed.Then,the paper combines LTL confined in finite traces and CEGAR technique to verify the programs.The paper has implemented the proposed approach,and exploited a new model verifier TPCHECKER,which supports the verification of temporal properties for C programs.Experimental results on benchmark programs show that the proposed approach performs well when verifying non-safety temporal properties of C programs.Meanwhile,extensive experiments illustrate that when checking safety properties via LTL specification,the approach is still competitive with the original tool where safety properties are verified by instrumenting programs with assertions.Finally,model checking is useful in discovering flaws in programs.In this domain,a desired property is often specified as a temporal logic formula or an assertion inserted at a proper position in the program.If a possible execution in the program violates a specified property,it is reported as a counterexample.Hence,finding the counterexamples quickly is a significant issue in software model checking.The main challenge in counterexample detection is loops in programs,as the computation and data related to loops can result in the rapid rise of state space meaning that most tools available will run out of memory or return an imprecise result when a deep loop is encountered.In order to further advance the efficiency and reduce state space,the paper proposes a hybrid technique that not only produces counterexamples quickly,but also maintains high levels of the precision,which combines dynamic and static analysis.First,Loops are classified into simple loops and complex loops by rules.Then,the paper replaces loop unwinding with loop summarizations for simple loops,and applies dynamic execution to deal with complex loops for accelerating to find counterexamples.To evaluate its performance in practice,we implemented the proposed approach to a tool named HYVER.Extensive experiments on a lot of benchmark programs show that our approach is useful in accelerating counterexample detection in software model checking.