Using Test Ranges to Improve Symbolic Execution

  • Rui Qiu
  • Sarfraz Khurshid
  • Corina S. Păsăreanu
  • Junye Wen
  • Guowei YangEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


Symbolic execution is a powerful systematic technique for checking programs, which has received a lot of research attention during the last decade. In practice however, the technique remains hard to scale. This paper introduces SynergiSE, a novel approach to improve symbolic execution by tackling a key bottleneck to its wider adoption: costly and incomplete constraint solving. To mitigate the cost, SynergiSE introduces a succinct encoding of constraint solving results, thereby enabling symbolic execution to be distributed among different workers while sharing and re-using constraint solving results among them without having to communicate databases of constraint solving results. To mitigate the incompleteness, SynergiSE introduces an integration of complementary approaches for testing, e.g., search-based test generation, with symbolic execution, thereby enabling symbolic execution and other techniques to apply in tandem. Experimental results using a suite of Java programs show that SynergiSE presents a promising approach for improving symbolic execution.



This work was funded in part by the National Science Foundation (NSF Grant Nos. CCF-1319688, CCF-1319858, CCF-1549161, CCF-1464123, and CNS-1239498).


  1. 1.
  2. 2.
  3. 3.
    Albert, E., Gómez-Zamalloa, M., Rojas, J.M., Puebla, G.: Compositional CLP-based test data generation for imperative languages. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 99–116. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  4. 4.
    Anand, S., Burke, E.K., Chen, T.Y., Clark, J., Cohen, M.B., Grieskamp, W., Harman, M., Harrold, M.J., Mcminn, P.: An orchestrated survey of methodologies for automated software test case generation. J. Syst. Softw. 86(8), 1978–2001 (2013)CrossRefGoogle Scholar
  5. 5.
    Baars, A.I., Harman, M., Hassoun, Y., Lakhotia, K., McMinn, P., Tonella, P., Vos, T.E.J.: Symbolic search-based testing. In: ASE 2011, pp. 53–62 (2011)Google Scholar
  6. 6.
    Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195–211. Springer, Cham (2016). CrossRefGoogle Scholar
  7. 7.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA 2002, pp. 123–133 (2002)Google Scholar
  8. 8.
    Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys 2011, pp. 183–198 (2011)Google Scholar
  9. 9.
    Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209–224 (2008)Google Scholar
  10. 10.
    Chen, J., Hu, W., Zhang, L., Hao, D., Khurshid, S., Liu, X., Zhang, L.: Learning to accelerate symbolic execution via code transformation. Under peer-reviewGoogle Scholar
  11. 11.
    Clarke, L.A.: A program testing system. In: ACM 1976, pp. 488–491 (1976)Google Scholar
  12. 12.
    Dini, N.: MKorat: a novel approach for memorizing the Korat search and some potential applications. Master’s thesis, University of Texas at Austin (2016)Google Scholar
  13. 13.
    Dong, S., Olivo, O., Zhang, L., Khurshid, S.: Studying the influence of standard compiler optimizations on symbolic execution. In: ISSRE 2015, pp. 205–215 (2015)Google Scholar
  14. 14.
    Message Passing Interface Forum: MPI: a message-passing interface standard. Technical report, Knoxville, TN, USA (1994)Google Scholar
  15. 15.
    Fraser, G., Arcuri, A.: Evolutionary generation of whole test suites. In: QSIC 2011, Los Alamitos, CA, USA, pp. 31–40 (2011)Google Scholar
  16. 16.
    Godefroid, P.: Compositional dynamic test generation. In: POPL 2007, pp. 47–54 (2007)Google Scholar
  17. 17.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI 2005, pp. 213–223 (2005)Google Scholar
  18. 18.
    Inkumsah, K., Xie, T.: Evacon: a framework for integrating evolutionary and concolic testing for object-oriented programs. In: ASE 2007, pp. 425–428 (2007)Google Scholar
  19. 19.
    Inkumsah, K., Xie, T.: Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: ASE 2008, pp. 297–306 (2008)Google Scholar
  20. 20.
    Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRefGoogle Scholar
  21. 21.
    Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003). CrossRefGoogle Scholar
  22. 22.
    Kim, M., Kim, Y., Rothermel, G.: A scalable distributed concolic testing approach: an empirical evaluation. In: ICST 2012, pp. 340–349 (2012)Google Scholar
  23. 23.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Lakhotia, K., McMinn, P., Harman, M.: An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. J. Syst. Softw. 83(12), 2379–2391 (2010)CrossRefGoogle Scholar
  25. 25.
    Li, G., Andreasen, E., Ghosh, I.: SymJS: automatic symbolic testing of Javascript web applications. In: FSE 2014, pp. 449–459 (2014)Google Scholar
  26. 26.
    Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: a symbolic execution engine for boogie programs. In: ICST 2016, pp. 45–56 (2016)Google Scholar
  27. 27.
    Ma, K.-K., Yit Phang, K., Foster, J.S., Hicks, M.: Directed symbolic execution. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 95–111. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  28. 28.
    Pacheco, C., Ernst, M.D.: Eclat: automatic generation and classification of test inputs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 504–527. Springer, Heidelberg (2005). CrossRefGoogle Scholar
  29. 29.
    Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE 2007, Minneapolis, MN, USA, 23–25 May 2007, pp. 75–84 (2007)Google Scholar
  30. 30.
    Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI 2011, pp. 504–515 (2011)Google Scholar
  31. 31.
    Păsăreanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA 2008, pp. 15–25 (2008)Google Scholar
  32. 32.
    Păsăreanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: ASE 2010, pp. 179–180 (2010)Google Scholar
  33. 33.
    Qiu, R., Khurshid, S., Păsăreanu, C.S., Yang, G.: A synergistic approach for distributed symbolic execution using test ranges. In: ICSE 2017 - Companion, pp. 130–132 (2017)Google Scholar
  34. 34.
    Qiu, R., Yang, G., Păsăreanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: ICSE 2015, pp. 632–642 (2015)Google Scholar
  35. 35.
    Rojas, J.M., Păsăreanu, C.S.: Compositional symbolic execution through program specialization. In: BYTECODE 2013 (ETAPS) (2013)Google Scholar
  36. 36.
    Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  37. 37.
    Shafi, A., Carpenter, B., Baker, M.: Nested parallelism for multi-core HPC systems using Java. J. Parallel Distrib. Comput. 69(6), 532–545 (2009)CrossRefGoogle Scholar
  38. 38.
    Siddiqui, J.H., Khurshid, S.: ParSym: parallel symbolic execution. In: ICSTE 2010, vol. 1, pp. V1-405–V1-409, October 2010Google Scholar
  39. 39.
    Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: OOPSLA 2012, pp. 523–536 (2012)Google Scholar
  40. 40.
    Slabý, J., Strejček, J., Trtík, M.: Checking properties described by state machines: on synergy of instrumentation, slicing, and symbolic execution. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 207–221. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  41. 41.
    Souza, M., Borges, M., d’Amorim, M., Păsăreanu, C.S.: CORAL: solving complex constraints for symbolic pathfinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359–374. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  42. 42.
    Staats, M., Pǎsǎreanu, C.: Parallel symbolic execution for structural test generation. In ISSTA 2010, pp. 183–194 (2010)Google Scholar
  43. 43.
    Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: FSE 2012, pp. 58:1–58:11 (2012)Google Scholar
  44. 44.
    Wang, R., Ning, P., Xie, T., Chen, Q.: MetaSymploit: day-one defense against script-based attacks with security-enhanced symbolic analysis. In: USENIX Security 2013, pp. 65–80 (2013)Google Scholar
  45. 45.
    Yang, G., Khurshid, S., Person, S., Rungta, N.: Property differencing for incremental checking. In: ICSE 2014, pp. 1059–1070 (2014)Google Scholar
  46. 46.
    Yang, G., Păsăreanu, C.S., Khurshid, S.: Memoized symbolic execution. In ISSTA 2012, pp. 144–154 (2012)Google Scholar
  47. 47.
    Yang, G., Person, S., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. ACM Trans. Softw. Eng. Methodol. 24(1), 3:1–3:42 (2014)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Rui Qiu
    • 1
  • Sarfraz Khurshid
    • 1
  • Corina S. Păsăreanu
    • 2
  • Junye Wen
    • 3
  • Guowei Yang
    • 3
    Email author
  1. 1.University of Texas at AustinAustinUSA
  2. 2.CMU/NASA AmesMountain ViewUSA
  3. 3.Texas State UniversitySan MarcosUSA

Personalised recommendations