Concolic testing

ABSTRACT

Concolic testing automates test input generation by combining the concrete and symbolic (concolic) execution of the code under test. Traditional test input generation techniques use either (1) concrete execution or (2) symbolic execution that builds constraints and is followed by a generation of concrete test inputs from these constraints. In contrast, concolic testing tightly couples both concrete and symbolic executions: they run simultaneously, and each gets feedback from the other.

We have implemented concolic testing in tools for testing both C and Java programs. We have used the tools to find bugs in several real-world software systems including SGLIB, a popular C data structure library used in a commercial tool, a third-party implementation of the Needham-Schroeder protocol and the TMN protocol, the scheduler of Honeywell's DEOS real-time operating system, and the Sun Microsystems' JDK 1.4 collection framework. In this tutorial, we will describe concolic testing and some of its recent extensions

References

1. D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. Generating Test from Counterexamples. In Proc. of the 26th ICSE, pages 326--335, 2004.
2. D. Bird and C. Munoz. Automatic Generation of Random Self-Checking Test Cases. IBM Systems Journal, 22(3):229--245, 1983.
3. K. Claessen and J. Hughes. Quickcheck: A lightweight tool for random testing of Haskell programs. In Proc. of 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 268--279, 2000.
4. L. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. Software Eng., 2:215--222, 1976.
5. P. D. Coward. Symbolic execution systems-a review. Software Engineering Journal, 3(6):229--239, 1988.
6. C. Csallner and Y. Smaragdakis. JCrasher: an automatic robustness tester for Java. Software: Practice and Experience, 34:1025--1050, 2004.
7. J. E. Forrester and B. P. Miller. An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In Proceedings of the 4th USENIX Windows System Symposium, 2000.
8. P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), 2005.
9. S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th Int. Conf. on TACAS, pages 553--568, 2003.
10. J. C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385--394, 1976.
11. G. Lee, J. Morris, K. Parker, G. A. Bundell, and P. Lam. Using symbolic execution to guide test generation: Research articles. Softw. Test. Verif. Reliab., 15(1):41--61, 2005.
12. R. Majumdar and K. Sen. Hybrid concolic testing. In 29th International Conference on Software Engineering (ICSE'07), pages 416--426. IEEE, 2007.
13. The economic impacts of inadequate infrastructure for software testing. National Institute of Standards and technology, Planning Report 02-3, May 2002.
14. J. Offut and J. Hayes. A Semantic Model of Program Faults. In Proc. of ISSTA'96, pages 195--200, 1996.
15. L. Osterweil. Integrating the testing, analysis and debugging of programs. In Proc. of a symposium on Software validation: inspection-testing verification-alternatives, pages 73--102, New York, NY, USA, 1984. Elsevier North-Holland, Inc.
16. C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In 19th European Conference Object-Oriented Programming, 2005.
17. K. Sen and G. Agha. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In Computer Aided Verification (CAV'06), LNCS, 2006. (To Appear).
18. K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'05). ACM, 2005.
19. W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with Java PathFinder. In Proc. 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97--107, 2004.
20. S. Visvanathan and N. Gupta. Generating test data for functions with pointer inputs. In 17th IEEE International Conference on Automated Software Engineering, 2002.
21. T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Procs. of TACAS, 2005.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging