Paper Info
Title
Model checking, testing and verification working together
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.
Year
DOI
Venue
2005
10.1007/s00165-005-0059-8
Formal Asp. Comput.
Keywords
Field
DocType
Model checking,Test generation,Verification
Programming language,Model checking,Computer science,Program behavior,Unit testing,Algorithm,Theoretical computer science,Runtime verification,Test case,Modular design,Path condition,Statistical hypothesis testing
Journal
Volume
Issue
ISSN
17
2
0934-5043
Citations 
PageRank 
References 
21
1.35
12
Authors
2
Name
Order
Citations
PageRank
Elsa L. Gunter144751.38
Doron Peled23357273.18