A CEGAR-Based Static-Dynamic Approach to Verifying Full Regular Properties of C Programs

In this article, we present an approach based on counterexample-guided abstraction refinement to verifying full regular temporal properties of C programs by means of combining both static analysis and dynamic verification. To this end, a desired property is specified by a propositional projection temporal logic formula $p$, and the labeled normal form graph (LNFG) of $\lnot p$ is automatically produced. Furthermore, the control flow automaton of the C program is constructed, and an enriched abstract reachability tree is generated under the guidance of the LNFG. Throughout the construction of the eART, whenever a candidate counterexample $cp$ is found, a verification input w.r.t $cp$ is generated by the SMT solver Z3. Subsequently, the C program is converted into a modeling, simulation, and verification language (MSVL) program $m$, and $\lnot p$ is also transformed to an MSVL program $m^{\prime }$. As a result, $m\; \text{and} \;m^{\prime }$ is executed to check whether the counterexample is spurious. The $cp$ is returned if it is a real counterexample; otherwise, the eART is refined. This process is repeated until no counterexample is found, namely the property is valid, or the counterexample is a real one The proposed approach enables us to not only verify full regular properties of C programs, but also produce precise results, neither false negatives nor false positives. The approach has been implemented in a tool named SDMC. Experiments show that SDMC outperforms the relevant tools available.