Counterexample-guided Spatial Flow Model Checking Methods for C Code
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Software verification has always been a popular research topic to ensure the correctness and security of software. However, due to the complex semantics and syntax of programming languages, the formal methods for verifying the correctness of programs have the problems of low accuracy and low efficiency. In particular, the state change in address space caused by pointer operations makes it difficult to guarantee the verification accuracy of existing model checking methods. By combining model checking and sparse value-flow analysis, this paper designs a spatial flow model to effectively describe the state behavior of C code at the symbolic-variable level and address-space level and proposes a model checking algorithm of CounterExample-Guided Abstraction refinement and Sparse value-flow strong update (CEGAS), which enables points-to-sensitive formal verification for C code. This paper establishes a C-code benchmark containing a variety of pointer operations and conducts comparative experiments on the basis of this benchmark. These experiments indicate that in the task of analyzing multi-class C code features, the model checking algorithm CEGAS proposed in this paper can achieve outstanding results compared with the existing model checking tools. The verification accuracy of CEGAS is 92.9%, and the average verification time of each line of code is 2.58 ms, both of which are better than those of existing verification tools.

    Reference
    Related
    Cited by
Get Citation

Yinbo Yu, Jiajia Liu, Dejun Mu. Counterexample-guided Spatial Flow Model Checking Methods for C Code. International Journal of Software and Informatics, 2022,12(3):263~284

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 29,2021
  • Revised:October 16,2021
  • Adopted:January 10,2022
  • Online: September 23,2022
  • Published: