Issue No. 01 - January/February (2011 vol. 37)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.23
Tsong Yueh Chen , Swinburne University of Technology, Hawthorn
T.H. Tse , The University of Hong Kong, Hong Kong
Zhi Quan Zhou , University of Wollongong, Wollongong
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 are satisfied 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.
Software/program verification, symbolic execution, testing and debugging.
T. Tse, T. Y. Chen and Z. Quan Zhou, "Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging," in IEEE Transactions on Software Engineering, vol. 37, no. , pp. 109-125, 2010.