An Approach to Verification Witness by Information Reuse
Abstract— Software Testing is vital as it guarantees correct operation of the software being developed. One of the most promising techniques used in Software Testing is Model Checking which ranges from software analysis to mathematical proofs. Formal verification is an emerging trend in Model Checking that determines if a correctness property holds for a system by exhaustively exploring the reachable states of a program. In contrast, if the property does not hold, a counterexample is generated, an execution trace leading to a state in which the property is violated. This approach becomes less efficient for large state space of software programs during direct analysis, such as explicit state analysis and predicate analysis. So the reuse of verification results is inevitable as they can save a significant amount of resources such as CPU time and Memory. A new approach is proposed for verification witnesses (proof certificates as well as counterexamples) in order to make information reuse practically applicable. Conditional Model Checking and Precision Reuse are the techniques that have paved way to this approach. The proposed approach demands to produce a counterexample in machine readable format so that it can be re-verified later against the original program.
Index Terms— Conditional Model Checking, Counterexample, Machine Readable Format, Precision Reuse
Click Here
International Journal for Trends in Technology & Engineering © 2015 IJTET JOURNAL