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. Keywords: Software/program verification, symbolic execution, testing and debugging.

1. This work is supported in part by the General Research Fund of the Research Grants Council of Hong Kong (project no. 717308), a discovery grant of the Australian Research Council (project no. DP 0771733), and a small grant of the University of Wollongong. 2. Centre for Software Analysis and Testing, Swinburne University of Technology, Hawthorn 3122, Australia. 3. Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong. 4. (Corresponding author.) School of Computer Science and Software Engineering, University of Wollongong, Wollongong, NSW 2522, Australia. Email:

EVERY VISITOR COUNTS: