Dynamic Execution Based On CPAChecker For Program Verification

Model Checking is a kind of formal verification technique,which is used for system modeling and system analysis.Due to the increasing complexity of system and software,state explosion in model checking has become increasingly serious.The most extensive solution currently applied to this problem is counterexample-guided abstraction refinement(CEGAR).CPAChecker,a successful tool of model checking,has introduced CEGAR to solve predicate detection.Though CEGAR can effectively relieve state explosion,there are still deficiencies.First,as a representative of multi-type problem,type conversion is hard to detect without executing procedures.Second,when the system has been modeled,the abstraction technique assumes that all branches are reachable.Once a counterexample occurs,refinement would be invoked to eliminate the fake one.Introducing dynamic execution can eliminate many unnecessary paths and refinements.As a result,dynamic execution based on CPAChecker for program verification is proposed and implemented in CPAChecker.The method has realized partial dynamic execution based on CPAChecker.A program would be abstracted as a CFA when modeling.And the switch between dynamic execution and static detection is based on the determinism or non-determinism of the node in CFA.When analizing the CFA,dynamic execution will be applied to determine the unique successor of cunrrent branch if all variables have been assigned;otherwise it will be detected in an static way.Particularly,in order to take all advantages of dynamic execution,we prefer to judge all nodes in current program when a counterexample occurs.If all nodes are assigned,we take the program as unsafe without analysis.Only abstract nodes exist must we analyze the counterexample and refine the model.The method uses static detection to effectively restrict the size of system model,and uses dynamic execution to reduce furious counterexamples due to static detection and reduces a lot of unnecessary refinements.As a result,the method makes program verification in CPAChecker more efficient and accurate.