This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging
January/February 2011 (vol. 37 no. 1)
pp. 109-125
ASCII Text
x 
 
Tsong Yueh Chen, T.H. Tse, Zhi Quan Zhou, "Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging," IEEE Transactions on Software Engineering, vol. 37, no. 1, pp. 109-125, January/February, 2011.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2010.23,
author = {Tsong Yueh Chen and T.H. Tse and Zhi Quan Zhou},
title = {Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging},
journal ={IEEE Transactions on Software Engineering},
volume = {37},
number = {1},
issn = {0098-5589},
year = {2011},
pages = {109-125},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.23},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging
IS - 1
SN - 0098-5589
SP109
EP125
EPD - 109-125
A1 - Tsong Yueh Chen,
A1 - T.H. Tse,
A1 - Zhi Quan Zhou,
PY - 2011
KW - Software/program verification
KW - symbolic execution
KW - testing and debugging.
VL - 37
JA - IEEE Transactions on Software Engineering
ER -
 
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.

[1] Java PathFinder Home Page. http://babelfish.arc.nasa.gov/tracjpf, 2010.
[2] H. Agrawal, J.R. Horgan, S. London, and W.E. Wong, "Fault Localization Using Execution Slices Dataflow Tests," Proc. Sixth Int'l Symp. Software Reliability Eng., pp. 143-151, 1995.
[3] P.E. Ammann and J.C. Knight, "Data Diversity: An Approach to Software Fault Tolerance," IEEE Trans. Computers, vol. 37, no. 4, pp. 418-425, Apr. 1988.
[4] S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. Paradkar, and M.D. Ernst, "Finding Bugs in Dynamic Web Applications," Proc. 2008 ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 261-272, 2008.
[5] L. Baresi and M. Young, "Test Oracles," Technical Report CIS-TR01-02, Dept. of Computer and Information Science, Univ. of Oregon, 2001.
[6] B. Beizer, Software Testing Techniques. Van Nostrand Reinhold, 1990.
[7] M. Blum and S. Kannan, "Designing Programs that Check Their Work," Proc. 31st Ann. ACM Symp. Theory of Computing, pp. 86-97, 1989, also J. ACM, vol. 42, no. 1, pp. 269-291, 1995.
[8] M. Blum, M. Luby, and R. Rubinfeld, "Self-Testing/Correcting with Applications to Numerical Problems," Proc. 22nd Ann. ACM Symp. Theory of Computing, pp. 73-83, 1990, also J. Computer and System Sciences, vol. 47, no. 3, pp. 549-595, 1993.
[9] B. Burgstaller, B. Scholz, and J. Blieberger, "Symbolic Analysis of Imperative Programming Languages," Modular Programming Languages, pp. 172-194. Springer, 2006.
[10] W.K. Chan, T.Y. Chen, H. Lu, T.H. Tse, and S.S. Yau, "Integration Testing of Context-Sensitive Middleware-Based Applications: A Metamorphic Approach," Int'l J. Software Eng. and Knowledge Eng., vol. 16, no. 5, pp. 677-703, 2006.
[11] W.K. Chan, S.C. Cheung, and K.R.P.H. Leung, "A Metamorphic Testing Approach for Online Testing of Service-Oriented Software Applications," Int'l J. Web Services Research, vol. 4, no. 2, pp. 60-80, 2007.
[12] H.Y. Chen, T.H. Tse, F.T. Chan, and T.Y. Chen, "In Black and White: An Integrated Approach to Class-Level Testing of Object-Oriented Programs," ACM Trans. Software Eng. and Methodology, vol. 7, no. 3, pp. 250-295, 1998.
[13] H.Y. Chen, T.H. Tse, and T.Y. Chen, "TACCLE: A Methodology for Object-Oriented Software Testing at the Class and Cluster Levels," ACM Trans. Software Eng. and Methodology, vol. 10, no. 1, pp. 56-109, 2001.
[14] T.Y. Chen, S.C. Cheung, and S.M. Yiu, "Metamorphic Testing: A New Approach for Generating Next Test Cases," Technical Report HKUST-CS98-01, Dept. of Computer Science, Hong Kong Univ. of Science and Tech nology, 1998.
[15] T.Y. Chen, J. Feng, and T.H. Tse, "Metamorphic Testing of Programs on Partial Differential Equations: A Case Study," Proc. 26th Ann. Int'l Computer Software and Applications Conf., pp. 327-333, 2002.
[16] T.Y. Chen, D.H. Huang, T.H. Tse, and Z.Q. Zhou, "Case Studies on the Selection of Useful Relations in Metamorphic Testing," Proc. Fourth Ibero-Am. Symp. Software Eng. and Knowledge Eng., pp. 569-583, 2004.
[17] T.Y. Chen, T.H. Tse, and Z.Q. Zhou, "Semi-Proving: An Integrated Method Based on Global Symbolic Evaluation and Metamorphic Testing," ACM SIGSOFT Software Eng. Notes, vol. 27, no. 4, pp. 191-195, 2002.
[18] T.Y. Chen, T.H. Tse, and Z.Q. Zhou, "Fault-Based Testing without the Need of Oracles," Information and Software Technology, vol. 45, no. 1, pp. 1-9, 2003.
[19] L.A. Clarke and D.J. Richardson, "Symbolic Evaluation Methods: Implementations Applications," Computer Program Testing, B. Chandrasekaran and S. Radicchi, eds., pp. 65-102, Elsevier, 1981.
[20] W.J. Cody,Jr., and W. Waite, Software Manual for the Elementary Functions. Prentice Hall, 1980.
[21] A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzè, "Using Symbolic Execution for Verifying Safety-Critical Systems," ACM SIGSOFT Software Eng. Notes, vol. 26, no. 5, pp. 142-151, 2001.
[22] R.A. DeMillo and A.J. Offutt, "Constraint-Based Automatic Test Data Generation," IEEE Trans. Software Eng., vol. 17, no. 9, pp. 900-910, Sept. 1991.
[23] L. de Moura and N. Bjørner, "Z3: An Efficient SMT Solver," Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, Springer, 2008.
[24] L.K. Dillon, "Using Symbolic Execution for Verification of Ada Tasking Programs," ACM Trans. Programming Languages and Systems, vol. 12, no. 4, pp. 643-669, 1990.
[25] T. Fahringer and A. Požgaj, "${\rm P}^3{\rm T}+$ : A Performance Estimator for Distributed and Parallel Programs," Scientific Programming, vol. 8, no. 2, pp. 73-93, 2000.
[26] T. Fahringer and B. Scholz, "A Unified Symbolic Evaluation Framework for Parallelizing Compilers," IEEE Trans. Parallel and Distributed Systems, vol. 11, no. 11, pp. 1105-1125, Nov. 2000.
[27] T. Fahringer and B. Scholz, Advanced Symbolic Analysis for Compilers: New Techniques and Algorithms for Symbolic Program Analysis and Optimization. Springer, 2003.
[28] M. Geller, "Test Data as an Aid in Proving Program Correctness," Comm. ACM, vol. 21, no. 5, pp. 368-375, 1978.
[29] M.P. Gerlek, E. Stoltz, and M. Wolfe, "Beyond Induction Variables: Detecting and Classifying Sequences Using a Demand-Driven SSA Form," ACM Trans. Programming Languages and Systems, vol. 17, no. 1, pp. 85-122, 1995.
[30] P. Godefroid, M.Y. Levin, and D.A. Molnar, "Active Property Checking," Proc. Eighth ACM Int'l Conf. Embedded Software, pp. 207-216, 2008.
[31] P. Godefroid, "Compositional Dynamic Test Generation," ACM SIGPLAN Notices, vol. 42, no. 1, pp. 47-54, 2007.
[32] P. Godefroid, N. Klarlund, and K. Sen, "DART: Directed Automated Random Testing," ACM SIGPLAN Notices, vol. 40, no. 6, pp. 213-223, 2005.
[33] A. Gotlieb, "Exploiting Symmetries to Test Programs," Proc. 14th Int'l Symp. Software Reliability Eng., pp. 365-374, 2003.
[34] A. Gotlieb and B. Botella, "Automated Metamorphic Testing," Proc. 27th Ann. Int'l Computer Software and Applications Conf., pp. 34-40, 2003.
[35] B.S. Gulavani, T.A. Henzinger, Y. Kannan, A.V. Nori, and S.K. Rajamani, "SYNERGY: A New Algorithm for Property Checking," Proc. 14th ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 117-127, 2006.
[36] M.R. Haghighat and C.D. Polychronopoulos, "Symbolic Analysis for Parallelizing Compilers," ACM Trans. Programming Languages and Systems, vol. 18, no. 4, pp. 477-518, 1996.
[37] B. Hailpern and P. Santhanam, "Software Debugging, Testing, and Verification," IBM Systems J., vol. 41, no. 1, pp. 4-12, 2002.
[38] M. Hall,Jr., The Theory of Groups. AMS Chelsea, 1999.
[39] H. He and N. Gupta, "Automated Debugging Using Path-Based Weakest Preconditions," Fundamental Approaches to Software Engineering, pp. 267-280, Springer, 2004.
[40] W.E. Howden, "Reliability of the Path Analysis Testing Strategy," IEEE Trans. Software Eng., vol. 2, no. 3, pp. 208-215, Sept. 1976.
[41] M. Hutchins, H. Foster, T. Goradia, and T. Ostrand, "Experiments on the Effectiveness of Dataflow- and Controlflow-Based Test Adequacy Criteria," Proc. 16th Int'l Conf. Software Eng., pp. 191-200, 1994.
[42] J. Jaffar, S. Michaylov, P.J. Stuckey, and R.H.C. Yap, "The CLP(${\cal R}$ ) Language and System," ACM Trans. Programming Languages and Systems, vol. 14, no. 3, pp. 339-395, 1992.
[43] J.A. Jones, M.J. Harrold, and J. Stasko, "Visualization of Test Information to Assist Fault Localization," Proc. 24th Int'l Conf. Software Eng., pp. 467-477, 2002.
[44] S. Khurshid, C.S. Păsăreanu, and W. Visser, "Generalized Symbolic Execution for Model Checking and Testing," Proc. Ninth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2003.
[45] J. King, "Symbolic Execution and Program Testing," Comm. ACM, vol. 19, no. 7, pp. 385-394, 1976.
[46] B. Korel and J. Rilling, "Application of Dynamic Slicing in Program Debugging," Proc. Third Int'l Workshop Automatic Debugging, pp. 43-58, 1997.
[47] R.J. Lipton, "New Directions in Testing," Proc. DIMACS Workshop Distributed Computing and Cryptography, pp. 191-202, 1991.
[48] C. Liu, L. Fei, X. Yan, S.P. Midkiff, and J. Han, "Statistical Debugging: A Hypothesis Testing-Based Approach," IEEE Trans. Software Eng., vol. 32, no. 10, pp. 831-848, Oct. 2006.
[49] C. Liu, X. Yan, and J. Han, "Mining Control Flow Abnormality for Logic Error Isolation," Proc. Sixth SIAM Int'l Conf. Data Mining, 2006.
[50] A.J. Offutt and E.J. Seaman, "Using Symbolic Execution to Aid Automatic Test Data Generation," Systems Integrity, Software Safety, and Process Security: Proc. Fifth Ann. Conf. Computer Assurance, pp. 12-21, 1990.
[51] M. Pezzè and M. Young, Software Testing and Analysis: Process, Principles, and Techniques. Wiley, 2008.
[52] K. Sen, D. Marinov, and G. Agha, "CUTE: A Concolic Unit Testing Engine for C," ACM SIGSOFT Software Eng. Notes, vol. 30, no. 5, pp. 263-272, 2005.
[53] T.H. Tse, T.Y. Chen, and Z.Q. Zhou, "Testing of Large Number Multiplication Functions in Cryptographic Systems," Proc. First Asia-Pacific Conf. Quality Software, pp. 89-98, 2000.
[54] T.H. Tse, F.C.M. Lau, W.K. Chan, P.C.K. Liu, and C.K.F. Luk, "Testing Object-Oriented Industrial Software without Precise Oracles or Results," Comm. ACM, vol. 50, no. 8, pp. 78-85, 2007.
[55] E.J. Weyuker, "On Testing Non-Testable Programs," The Computer J., vol. 25, no. 4, pp. 465-470, 1982.
[56] S. Wolfram, The Mathematica Book. Wolfram Media, 2003.
[57] G. Yorsh, T. Ball, and M. Sagiv, "Testing, Abstraction Theorem Proving: Better Together!," Proc. 2006 ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 145-156, 2006.
[58] A. Zeller, "Isolating Cause-Effect Chains from Computer Programs," ACM SIGSOFT Software Eng. Notes, vol. 27, no. 6, pp. 1-10, 2002.
[59] A. Zeller and R. Hildebrandt, "Simplifying and Isolating Failure-Inducing Input," IEEE Trans. Software Eng., vol. 28, no. 2, pp. 183-200, Feb. 2002.
[60] Z.Q. Zhou, S. Zhang, M. Hagenbuchner, T.H. Tse, F.-C. Kuo, and T.Y. Chen, "Automated Functional Testing of Online Search Services," Software Testing, Verification and Reliability, 2010, doi:10.1002/stvr.437.

Index Terms:
Software/program verification, symbolic execution, testing and debugging.
Citation:
Tsong Yueh Chen, T.H. Tse, Zhi Quan Zhou, "Semi-Proving: An Integrated Method for Program Proving, Testing, and Debugging," IEEE Transactions on Software Engineering, vol. 37, no. 1, pp. 109-125, Jan.-Feb. 2011, doi:10.1109/TSE.2010.23
Usage of this product signifies your acceptance of the Terms of Use.