Back to Search
Start Over
A CEGAR-Based Static–Dynamic Approach to Verifying Full Regular Properties of C Programs.
- Source :
-
IEEE Transactions on Reliability . Dec2021, Vol. 70 Issue 4, p1455-1467. 13p. - Publication Year :
- 2021
-
Abstract
- 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. [ABSTRACT FROM AUTHOR]
- Subjects :
- *ROBOTS
*LOGIC
*TREES
*SEMANTICS
Subjects
Details
- Language :
- English
- ISSN :
- 00189529
- Volume :
- 70
- Issue :
- 4
- Database :
- Academic Search Index
- Journal :
- IEEE Transactions on Reliability
- Publication Type :
- Academic Journal
- Accession number :
- 153925844
- Full Text :
- https://doi.org/10.1109/TR.2021.3118877