Model checking, testing and verification working together

26Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.

Abstract

We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both the program counters and the program variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of the program counters, and (2) the formulation and refutation of a path condition, which inherits conditions constraining the program variables from the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing. © BCS 2005.

Cite

CITATION STYLE

APA

Gunter, E., & Peled, D. (2005). Model checking, testing and verification working together. Formal Aspects of Computing, 17(2), 201–221. https://doi.org/10.1007/s00165-005-0059-8

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free