Advertisement

On the Nature of Symbolic Execution

  • Frank S. de BoerEmail author
  • Marcello Bonsangue
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

In this paper, we provide a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. We first introduce such a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables.

Notes

Acknowledgements

This work arose out of our Foundation of Testing master course (LIACS) in 2018, and we thank the master students for their valuable comments. We thank the anonymous reviewers for their valuable comments.

References

  1. 1.
    King, C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Albert, E., Arenas, P., Gómez-Zamalloa, M., Rojas, J.M.: Test case generation by symbolic execution: basic concepts, a CLP-based instance, and actor-based concurrency. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 263–309. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-07317-0_7CrossRefGoogle Scholar
  3. 3.
    Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1–50:39 (2018)CrossRefGoogle Scholar
  4. 4.
    Lucanu, D., Rusu, V., Arusoaie, A.: A generic framework for symbolic execution: a coinductive approach. J. Symbolic Comput. 80(1), 125–163 (2017)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Braione, P., Denaro, G., Pezzè, M.: Symbolic execution of programs with heap inputs. In: Proceedings of the 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015), pp. 602–613. ACM (2015)Google Scholar
  6. 6.
    Trtík, M., Strejček, J.: Symbolic memory with pointers. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 380–395. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_27CrossRefGoogle Scholar
  7. 7.
    Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS 2006), pp. 322–335. ACM (2006)Google Scholar
  8. 8.
    Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI 2008), pp. 209–224, USENIX Association (2008)Google Scholar
  9. 9.
    Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: Proceedings of the 18th International Symposium on Software Testing and Analysis (ISSTA 2009), pp. 129–140. ACM (2009)Google Scholar
  10. 10.
    Perry, D.M., Mattavelli, A., Zhang, X., Cadar, C.: Accelerating array constraints in symbolic execution. In Proceedings of the 26th International Symposium on Software Testing and Analysis (ISSTA 2017), pp. 68–78. ACM (2017)Google Scholar
  11. 11.
    Deng, X., Lee, J.: Bogor/Kiasan: a K-bounded symbolic execution for checking strong heap properties of open systems. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), pp. 157–166 (2006)Google Scholar
  12. 12.
    de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_22CrossRefGoogle Scholar
  13. 13.
    Gries, D.: The Science of Programming. Texts and Monographs in Computer Science. Springer (1981)Google Scholar
  14. 14.
    Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-25271-6_8CrossRefGoogle Scholar
  15. 15.
    Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 365–381. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31980-1_24CrossRefzbMATHGoogle Scholar
  16. 16.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2005), pp. 213–223. ACM (2005)Google Scholar
  17. 17.
    Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2009), pp. 363–374. ACM (2009)Google Scholar
  18. 18.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbric, M.: Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Centrum Wiskunde & Informatica (CWI)AmsterdamThe Netherlands
  2. 2.Leiden Institute Of Advanced Computer Science (LIACS)LeidenThe Netherlands

Personalised recommendations