|IEEE Transactions on Software Engineering 37 (1): 109-125 (2011)|
T.Y. Chen 2 , T.H. Tse 3 , and Zhi Quan Zhou 4
[paper from IEEE Xplore | paper from IEEE digital library | technical report TR-2009-10]
We present an integrated method for program proving, testing, and debugging.
Using the concept of metamorphic relations,
we select necessary properties for target programs.
For programs where global symbolic evaluation can be conducted
and the constraint expressions involved can be solved,
we can either prove that these necessary conditions for program correctness
or identify all inputs
that violate the conditions.
For other programs,
our method can be converted into a symbolic testing approach.
Our method extrapolates from the correctness of a program for tested
inputs to the correctness of the program for related untested inputs.
The method supports automatic debugging through the identification
of constraint expressions that reveal failures.
Keywords: Software/program verification, symbolic execution, testing and debugging.
|EVERY VISITOR COUNTS:|