Cristian Cadar
Patrice Godefroid
Willem Visser
ABSTRACT
We present results for the "Impact Project Focus Area" on the topic of symbolic execution as used in software testing. Symbolic execution is a program analysis technique introduced in the 70s that has received renewed interest in recent years, due to algorithmic advances and increased availability of computational power and constraint solving technology. We review classical symbolic execution and some modern extensions such as generalized symbolic execution and dynamic test generation. We also give a preliminary assessment of the use in academia, research labs, and industry.
- S. Anand, C. S. Păsăreanu, and W. Visser. JPF-SE: a symbolic execution extension to Java PathFinder. In TACAS'07, pages 134--138, 2007. Google Scholar
Digital Library
- S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. Paradkar, and M. D. Ernst. Finding bugs in dynamic web applications. In ISSTA'08, July 2008. Google ScholarDigital Library
- T. Avgerinos, S. K. Cha, B. L. T. Hao, and D. Brumley. AEG: Automatic exploit generation. In NDSS'11, Feb 2011.Google Scholar
- M. Baluda, P. Braione, G. Denaro, and M. Pezzé. Structural coverage of feasible code. In AST'10, pages 59--66. ACM, 2010. Google ScholarDigital Library
- D. Bethea, R. Cochran, and M. Reiter. Server-side verification of client behavior in online games. In NDSS'10, Feb-Mar 2010.Google Scholar
- N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis for string-manipulating programs. In TACAS'09, Mar. 2009. Google ScholarDigital Library
- P. Boonstoppel, C. Cadar, and D. Engler. RWset: Attacking path explosion in constraint-based test generation. In TACAS'08, Mar-Apr 2008. Google ScholarDigital Library
- R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT - a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234--245, 1975. Google ScholarDigital Library
- J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In ASE'08, 2008. Google ScholarDigital Library
- W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software - Practice and Experience, 30(7):775--802, 2000. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI'08, Dec 2008. Google ScholarDigital Library
- C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself (invited paper). In SPIN'05, Aug 2005. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: Automatically generating inputs of death. In CCS'06, Oct-Nov 2006. Google ScholarDigital Library
- V. Chipounov and G. Candea. Reverse engineering of binary device drivers with RevNIC. In EuroSys'10, Apr 2010. Google ScholarDigital Library
- L. A. Clarke. A program testing system. In Proc. of the 1976 annual conference, pages 488--491, 1976. Google ScholarDigital Library
- L. A. Clarke and D. J. Richardson. Program Flow Analysis: Theory and Application (Symbolic Evaluation Methods for Program Analysis). S. Muchnick and N. Jones, Prentice Hall, 1981. Google ScholarDigital Library
- L. A. Clarke and D. J. Richardson. Applications of symbolic evaluation. Journal of Systems and Software, 5(1):15--35, 1985. Google ScholarDigital Library
- A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzé. Using symbolic execution for verifying safety-critical systems. In ESEC/FSE'01, 2001. Google ScholarDigital Library
- P. D. Coward. Symbolic execution systems - a review. Softw. Eng. J., 3:229--239, November 1988. Google ScholarDigital Library
- H. Cui, J. Wu, C. che Tsai, and J. Yang. Stable deterministic multithreading through schedule memoization. In OSDI'10, 2010. Google ScholarDigital Library
- J. de Halleux and N. Tillmann. Moles: Tool-assisted environment isolation with closures. In TOOLS'10, June-July 2010. Google ScholarDigital Library
- L. de Moura and N. Bjorner. Z3: An Efficient SMT Solver. In TACAS'08, Mar-Apr 2008. Google ScholarDigital Library
- X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In ASE'06, 2006. Google ScholarDigital Library
- L. K. Dillon. Using symbolic execution for verification of Ada tasking programs. ACM TOPLAS, 12, October 1990. Google ScholarDigital Library
- V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In CAV'07, July 2007. Google ScholarDigital Library
- P. Godefroid. Compositional dynamic test generation. In Proc. of the ACM POPL, Jan 2007. Google ScholarDigital Library
- P. Godefroid. Software model checking improving security of a billion computers. In SPIN'09, June 2009. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI'05, June 2005. Google ScholarDigital Library
- P. Godefroid, M. Levin, and D. Molnar. Automated Whitebox Fuzz Testing. In NDSS'08, Feb. 2008.Google Scholar
- L. J. Harrison and R. A. Kemmerer. An interleaving symbolic execution approach for the formal verification of Ada programs with tasking. In Ada Applications and Environments'88, 1988.Google ScholarCross Ref
- W. Howden. Symbolic testing and the DISSECT symbolic evaluation system. IEEE Transactions on Software Engineering, 3(4):266--278, 1977. Google ScholarDigital Library
- K. Jayaraman, D. Harvison, V. Ganesh, and A. Kiezun. jFuzz: A concolic whitebox fuzzer for Java. In In NFM'09, Apr. 2009.Google Scholar
- S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS'03, Apr. 2003. Google ScholarDigital Library
- Y. Kim, M. Kim, and N. Dang. Scalable distributed concolic testing: a case study on a flash storage platform. In ICTAC'10, pages 199--213, 2010. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Commun. ACM, 19:385--394, July 1976. Google ScholarDigital Library
- B. Korel. A Dynamic Approach of Test Data Generation. In IEEE Conference on Software Maintenance, Nov 1990.Google Scholar
- V. Kuznetsov, V. Chipounov, and G. Candea. Testing closed-source binary device drivers with DDT. In USENIX ATC'10, June 2010. Google ScholarDigital Library
- K. Lakhotia, N. Tillmann, M. Harman, and J. de Halleux. Flopsy - search-based floating point constraint solving for symbolic execution. In ICTSS'10, pages 142--157, 2010. Google ScholarDigital Library
- C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In CGO'04, Mar 2004. Google ScholarDigital Library
- R. Majumdar and K. Sen. Hybrid concolic testing. In ICSE'07, May 2007. Google ScholarDigital Library
- R. Majumdar and R.-G. Xu. Reducing test inputs using information partitions. In CAV'09, pages 555--569, 2009. Google ScholarDigital Library
- D. Molnar, X. C. Li, and D. Wagner. Dynamic test generation to find integer bugs in x86 binary linux programs. In USENIX Security'09, Aug 2009. Google ScholarDigital Library
- C. Pasareanu, P. Mehlitz, D. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In ISSTA'08, July 2008. Google ScholarDigital Library
- C. S. Pasareanu and W. Visser. A survey of new trends in symbolic execution for software testing and analysis. STTT, 11(4):339--353, 2009. Google ScholarDigital Library
- S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In PLDI'11 (to appear), June 2011. Google ScholarDigital Library
- C. Ramamoorthy, S.-B. Ho, and W. Chen. On the automated generation of program test data. IEEE Trans. on Software Engineering, 2(4):293--300, 1976. Google ScholarDigital Library
- M. Ruse, T. Sarkar, and S. Basu. Analysis & detection of SQL injection vulnerabilities via automatic test case generation of programs. In SAINT'10, July 2010. Google ScholarDigital Library
- R. Sasnauskas, J. A. B. Link, M. H. Alizai, and K. Wehrle. Kleenet: automatic bug hunting in sensor network applications. In IPSN'10, Apr 2010.Google Scholar
- E. J. Schwartz, T. Avgerinos, and D. Brumley. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In IEEE Symposium on Security and Privacy, May 2010. Google ScholarDigital Library
- K. Sen. Scalable Automated Methods for Dynamic Program Analysis. PhD thesis, University of Illinois at Urbana-Champaign, June 2006. Google ScholarDigital Library
- K. Sen and G. Agha. CUTE and jCUTE : Concolic unit testing and explicit path model-checking tools. In CAV'06, 2006. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE'05, Sep 2005. Google ScholarDigital Library
- J. H. Siddiqui and S. Khurshid. ParSym: Parallel symbolic execution. In ICSTE'10, Oct. 2010.Google ScholarCross Ref
- S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM TOSEM, 17:10:1--10:34, May 2008. Google ScholarDigital Library
- M. Souza, M. Borges, M. d'Amorim, and C. Păsăreanu. Coral: Solving complex constraints for symbolic pathfinder. In NFM'11 (to appear), Apr. 2011. Google ScholarDigital Library
- M. Staats and C. S. Pasareanu. Parallel symbolic execution for structural test generation. In ISSTA'10, July 2010. Google ScholarDigital Library
- N. Tillmann and J. de Halleux. Pex - white box test generation for .NET. In TAP'08, Apr 2008. Google ScholarDigital Library
- N. Tillmann and W. Schulte. Parameterized unit tests. In ESEC/FSE'05, Sept. 2005. Google ScholarDigital Library
- W. Visser, C. S. Păsăreanu, and R. Pelánek. Test input generation for java containers using state matching. In ISSTA'06, July 2006. Google ScholarDigital Library
- T. Xie. Improving automation in developer testing: State of practice. Technical report, North Carolina State University, 2009.Google Scholar
- T. Xie, N. Tillmann, P. de Halleux, and W. Schulte. Fitness-guided path exploration in dynamic symbolic execution. In DSN'09, June-July 2009.Google ScholarCross Ref
- Z. Xu, Y. Kim, M. Kim, G. Rothermel, and M. B. Cohen. Directed test suite augmentation: techniques and tradeoffs. In FSE'10, Nov. 2010. Google ScholarDigital Library
- J. Yang, C. Sar, P. Twohey, C. Cadar, and D. Engler. Automatically generating malicious disks using symbolic execution. In IEEE Symposium on Security and Privacy, May 2006. Google ScholarDigital Library
- C. Zamfir and G. Candea. Execution synthesis: A technique for automated software debugging. In EuroSys'10, Apr 2010. Google ScholarDigital Library
Index Terms
- Symbolic execution for software testing in practice: preliminary assessment
Recommendations
Symbolic execution and program testing
This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be ...
Automatic testing of symbolic execution engines via program generation and differential testing
ASE '17: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software EngineeringSymbolic execution has attracted significant attention in recent years, with applications in software testing, security, networking and more. Symbolic execution tools, like CREST, KLEE, FuzzBALL, and Symbolic PathFinder, have enabled researchers and ...
Veritesting Challenges in Symbolic Execution of Java
Scaling symbolic execution to industrial-sized programs is an important open research problem. Veritesting is a promising technique that improves scalability by combining the advantages of static symbolic execution with those of dynamic symbolic ...
Comments