Predicate abstraction techniques have been shown to be a powerful technique for verifying imperative programs, which can solve the problem of state space explosion pretty well. Among them, lazy abstraction with interpolation-based refinement also called the IMPACT approach has gained increasing popularity in the last years. However, despite its high efficiency, the IMPACT fails to work out some kinds of the programs because the interpolants produced by interpolant solver are so bad to make the verification divergent. According to the features of some of these programs, we extend the IMPACT method to make it applicable for them. In addition to its basic ones, two other operations are introduced to the IMPACT refinement to guide it produce reasonal interpolants which are helpful for the verification process to converge. The experiments on the benchmark of SV-COMP2020 show the potential of the extended approach.

Program verification techniques have gained increasing popularity in academic and industrial circles during the last years. Predicate abstraction is a traditional and practical verification technique, which can solve the problem of state space explosion pretty well. Many software verification tools have implemented it. But these implementations are not user-friendly, or scalable. Aimed at these problems, we describe and implement a new automatic predicate abstraction framework, CChecker, for proving the safety of procedural programs with integer assignments. CChecker is a whole system composed of two parts: front and back end. The front end preprocesses and parses the source programs into logic models based on Clang. And the back end resolves the models based on Z3 to get software safety property. At last, the experiments show the potential of CChecker.