
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Tsong Yueh Chen, T.H. Tse, Zhi Quan Zhou, "SemiProving: An Integrated Method for Program Proving, Testing, and Debugging," IEEE Transactions on Software Engineering, vol. 37, no. 1, pp. 109125, January/February, 2011.  
BibTex  x  
@article{ 10.1109/TSE.2010.23, author = {Tsong Yueh Chen and T.H. Tse and Zhi Quan Zhou}, title = {SemiProving: An Integrated Method for Program Proving, Testing, and Debugging}, journal ={IEEE Transactions on Software Engineering}, volume = {37}, number = {1}, issn = {00985589}, year = {2011}, pages = {109125}, 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  SemiProving: An Integrated Method for Program Proving, Testing, and Debugging IS  1 SN  00985589 SP109 EP125 EPD  109125 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   
[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. 143151, 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. 418425, 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. 261272, 2008.
[5] L. Baresi and M. Young, "Test Oracles," Technical Report CISTR0102, 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. 8697, 1989, also J. ACM, vol. 42, no. 1, pp. 269291, 1995.
[8] M. Blum, M. Luby, and R. Rubinfeld, "SelfTesting/Correcting with Applications to Numerical Problems," Proc. 22nd Ann. ACM Symp. Theory of Computing, pp. 7383, 1990, also J. Computer and System Sciences, vol. 47, no. 3, pp. 549595, 1993.
[9] B. Burgstaller, B. Scholz, and J. Blieberger, "Symbolic Analysis of Imperative Programming Languages," Modular Programming Languages, pp. 172194. Springer, 2006.
[10] W.K. Chan, T.Y. Chen, H. Lu, T.H. Tse, and S.S. Yau, "Integration Testing of ContextSensitive MiddlewareBased Applications: A Metamorphic Approach," Int'l J. Software Eng. and Knowledge Eng., vol. 16, no. 5, pp. 677703, 2006.
[11] W.K. Chan, S.C. Cheung, and K.R.P.H. Leung, "A Metamorphic Testing Approach for Online Testing of ServiceOriented Software Applications," Int'l J. Web Services Research, vol. 4, no. 2, pp. 6080, 2007.
[12] H.Y. Chen, T.H. Tse, F.T. Chan, and T.Y. Chen, "In Black and White: An Integrated Approach to ClassLevel Testing of ObjectOriented Programs," ACM Trans. Software Eng. and Methodology, vol. 7, no. 3, pp. 250295, 1998.
[13] H.Y. Chen, T.H. Tse, and T.Y. Chen, "TACCLE: A Methodology for ObjectOriented Software Testing at the Class and Cluster Levels," ACM Trans. Software Eng. and Methodology, vol. 10, no. 1, pp. 56109, 2001.
[14] T.Y. Chen, S.C. Cheung, and S.M. Yiu, "Metamorphic Testing: A New Approach for Generating Next Test Cases," Technical Report HKUSTCS9801, 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. 327333, 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 IberoAm. Symp. Software Eng. and Knowledge Eng., pp. 569583, 2004.
[17] T.Y. Chen, T.H. Tse, and Z.Q. Zhou, "SemiProving: An Integrated Method Based on Global Symbolic Evaluation and Metamorphic Testing," ACM SIGSOFT Software Eng. Notes, vol. 27, no. 4, pp. 191195, 2002.
[18] T.Y. Chen, T.H. Tse, and Z.Q. Zhou, "FaultBased Testing without the Need of Oracles," Information and Software Technology, vol. 45, no. 1, pp. 19, 2003.
[19] L.A. Clarke and D.J. Richardson, "Symbolic Evaluation Methods: Implementations Applications," Computer Program Testing, B. Chandrasekaran and S. Radicchi, eds., pp. 65102, Elsevier, 1981.
[20] W.J. Cody,Jr., and W. Waite, Software Manual for the Elementary Functions. Prentice Hall, 1980.
[21] A. CoenPorisini, G. Denaro, C. Ghezzi, and M. Pezzè, "Using Symbolic Execution for Verifying SafetyCritical Systems," ACM SIGSOFT Software Eng. Notes, vol. 26, no. 5, pp. 142151, 2001.
[22] R.A. DeMillo and A.J. Offutt, "ConstraintBased Automatic Test Data Generation," IEEE Trans. Software Eng., vol. 17, no. 9, pp. 900910, 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. 337340, 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. 643669, 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. 7393, 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. 11051125, 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. 368375, 1978.
[29] M.P. Gerlek, E. Stoltz, and M. Wolfe, "Beyond Induction Variables: Detecting and Classifying Sequences Using a DemandDriven SSA Form," ACM Trans. Programming Languages and Systems, vol. 17, no. 1, pp. 85122, 1995.
[30] P. Godefroid, M.Y. Levin, and D.A. Molnar, "Active Property Checking," Proc. Eighth ACM Int'l Conf. Embedded Software, pp. 207216, 2008.
[31] P. Godefroid, "Compositional Dynamic Test Generation," ACM SIGPLAN Notices, vol. 42, no. 1, pp. 4754, 2007.
[32] P. Godefroid, N. Klarlund, and K. Sen, "DART: Directed Automated Random Testing," ACM SIGPLAN Notices, vol. 40, no. 6, pp. 213223, 2005.
[33] A. Gotlieb, "Exploiting Symmetries to Test Programs," Proc. 14th Int'l Symp. Software Reliability Eng., pp. 365374, 2003.
[34] A. Gotlieb and B. Botella, "Automated Metamorphic Testing," Proc. 27th Ann. Int'l Computer Software and Applications Conf., pp. 3440, 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. 117127, 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. 477518, 1996.
[37] B. Hailpern and P. Santhanam, "Software Debugging, Testing, and Verification," IBM Systems J., vol. 41, no. 1, pp. 412, 2002.
[38] M. Hall,Jr., The Theory of Groups. AMS Chelsea, 1999.
[39] H. He and N. Gupta, "Automated Debugging Using PathBased Weakest Preconditions," Fundamental Approaches to Software Engineering, pp. 267280, Springer, 2004.
[40] W.E. Howden, "Reliability of the Path Analysis Testing Strategy," IEEE Trans. Software Eng., vol. 2, no. 3, pp. 208215, Sept. 1976.
[41] M. Hutchins, H. Foster, T. Goradia, and T. Ostrand, "Experiments on the Effectiveness of Dataflow and ControlflowBased Test Adequacy Criteria," Proc. 16th Int'l Conf. Software Eng., pp. 191200, 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. 339395, 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. 467477, 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. 385394, 1976.
[46] B. Korel and J. Rilling, "Application of Dynamic Slicing in Program Debugging," Proc. Third Int'l Workshop Automatic Debugging, pp. 4358, 1997.
[47] R.J. Lipton, "New Directions in Testing," Proc. DIMACS Workshop Distributed Computing and Cryptography, pp. 191202, 1991.
[48] C. Liu, L. Fei, X. Yan, S.P. Midkiff, and J. Han, "Statistical Debugging: A Hypothesis TestingBased Approach," IEEE Trans. Software Eng., vol. 32, no. 10, pp. 831848, 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. 1221, 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. 263272, 2005.
[53] T.H. Tse, T.Y. Chen, and Z.Q. Zhou, "Testing of Large Number Multiplication Functions in Cryptographic Systems," Proc. First AsiaPacific Conf. Quality Software, pp. 8998, 2000.
[54] T.H. Tse, F.C.M. Lau, W.K. Chan, P.C.K. Liu, and C.K.F. Luk, "Testing ObjectOriented Industrial Software without Precise Oracles or Results," Comm. ACM, vol. 50, no. 8, pp. 7885, 2007.
[55] E.J. Weyuker, "On Testing NonTestable Programs," The Computer J., vol. 25, no. 4, pp. 465470, 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. 145156, 2006.
[58] A. Zeller, "Isolating CauseEffect Chains from Computer Programs," ACM SIGSOFT Software Eng. Notes, vol. 27, no. 6, pp. 110, 2002.
[59] A. Zeller and R. Hildebrandt, "Simplifying and Isolating FailureInducing Input," IEEE Trans. Software Eng., vol. 28, no. 2, pp. 183200, 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.