DSD-Crasher: a hybrid analysis tool for bug finding

ABSTRACT

DSD-Crasher is a bug finding tool that follows a three-step approach to program analysis:

1. D. Capture the program's intended execution behavior with dynamic invariant detection. The derived invariants exclude many unwanted values from the program's input domain.
2. S. Statically analyze the program within the restricted input domain to explore many paths.
3. D. Automatically generate test cases that focus on verifying the results of the static analysis. Thereby confirmed results are never false positives, as opposed to the high false positive rate inherent in conservative static analysis.

.This three-step approach yields benefits compared to past two-step combinations in the literature. In our evaluation with third-party applications, we demonstrate higher precision over tools that lack a dynamic step and higher efficiency over tools that lack a static step.

REFERENCES

• 1: Apache Software Foundation. Bytecode engineering library (BCEL). http://jakarta.apache.org/bcel/, Apr. 2003. Accessed May 2006.
• 2: T. Ball. Abstraction-guided test generation: A case study. Technical Report MSR-TR-2003-86, Microsoft Research, Nov. 2003.
• 3: K. Beck and E. Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37--50, July 1998.
• 4: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 5: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 6: Yoonsik Cheon , Gary T. Leavens, A Simple and Practical Approach to Unit Testing: The JML and JUnit Way, Proceedings of the 16th European Conference on Object-Oriented Programming, p.231-255, June 10-14, 2002
• 7: D. R. Cok and J. R. Kiniry. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2. Technical Report NIII-R0413, Nijmegen Institute for Computing and Information Science, May 2004.
• 8: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 9: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, p.422-431, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 10: Christoph Csallner , Yannis Smaragdakis, Dynamically discovering likely interface invariants, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134435]
• 11: D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, Hewlett-Packard Systems Research Center, July 2003.
• 12: S. H. Edwards. A framework for practical, automated black-box testing of component-based software. Software Testing, Verification & Reliability, 11(2):97--111, June 2001.
• 13: M. D. Ernst. Static and dynamic analysis: Synergy and duality. In Proc. ICSE Workshop on Dynamic Analysis, pages 24--27, May 2003.
• 14: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 15: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 17: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 18: M. Hapner, R. Burridge, R. Sharma, and J. Fialli. Java message service: Version 1.1. Sun Microsystems, Inc., Apr. 2002.
• 19: David Hovemeyer , William Pugh, Finding bugs is easy, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028717]
• 20: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 21: D. Kroening, A. Groce, and E. M. Clarke. Counterexample guided abstraction refinement via program execution. In J. Davies, W. Schulte, and M. Barnett, editors, Formal Methods and Software Engineering: 6th International Conference on Formal Engineering Methods, pages 224--238. Springer, Nov. 2004.
• 22: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR98-06y, Department of Computer Science, Iowa State University, June 1998.
• 23: K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user's manual. Technical Report 2000-002, Compaq Computer Corporation Systems Research Center, Oct. 2000.
• 24: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 25: Jeremy W. Nimmer , Michael D. Ernst, Automatic generation of program specifications, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 26: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 27: C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In Proc. 19th European Conference on Object-Oriented Programming, pages 504--527, July 2005.
• 28: Parasoft Inc. Jtest. http://www.parasoft.com/, Oct. 2002. Accessed May 2006.
• 29: Nick Rutar , Christian B. Almazan , Jeffrey S. Foster, A Comparison of Bug Finding Tools for Java, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.245-256, November 02-05, 2004 [doi>10.1109/ISSRE.2004.1]
• 30: Sriram Sankar , Roger Hayes, ADL—an interface definition language for specifying and testing software, Proceedings of the workshop on Interface definition languages, p.13-21, August 1994, Portland, Oregon, United States
• 31: H. Schlenker and G. Ringwelski. POOC: A platform for object-oriented constraint programming. In Proc. Joint ERCIM/CologNet International Workshop on Constraint Solving and Constraint Logic Programming, pages 159--170, June 2002.
• 32: M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures with a constraint solver. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference, pages 505--520. Springer, Apr. 2003.
• 33: T. Xie and D. Notkin. Tool-assisted unit test selection based on operational violations. In Proc. 18th Annual International Conference on Automated Software Engineering (ASE 2003), pages 40--48, Oct. 2003.
• 34: Y. Xie and D. Engler. Using redundancies to find errors. IEEE Transactions on Software Engineering, 29(10):915--928, Oct. 2003.
• 35: M. Young. Symbiosis of static analysis and program testing. In Proc. 6th International Conference on Fundamental Approaches to Software Engineering, pages 1--5, Apr. 2003.
• 36: S. H. Zweben, W. D. Heym, and J. Kimmich. Systematic testing of data abstractions based on software specifications. Software Testing, Verification & Reliability, 1(4):39--55, Jan. 1992.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

Keywords:
automatic testing, bug finding, dynamic analysis, dynamic invariant detection, extended static checking, false positives, static analysis, test case generation, usability