Symbolic execution formally explained

Abstract

In this paper, we provide a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values.We first introduce a formalmodel for a basic programming languagewith 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 present a more general formal framework for proving the soundness and completeness of the symbolic execution of a basic object-oriented language which features dynamically allocated variables.

References

  1. [AAGR14]

    Albert Elvira, Arenas Puri, Gómez-Zamalloa Miguel, Rojas José Miguel (2014) Test case generation by symbolic execution: Basic concepts, a clp-based instance, and actor-based concurrency. In: Marco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Ina Schaefer (eds.), Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, Bertinoro, Italy, June 16-20, 2014, Advanced Lectures, volume 8483 of Lecture Notes in Computer Science. Springer, pp 263–309

  2. [ABB+16]

    Ahrendt Wolfgang, Beckert Bernhard, Bubel Richard, Hähnle Reiner, Schmitt Peter H, Ulbrich Mattias, (eds.) (2016) Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science. Springer

  3. [AdBO09]

    Apt Krzysztof R, de Boer Frank, Olderog Ernst-Rdiger (2009)Verification of Sequential and Concurrent Programs, 3rd edition. Springer

  4. [BCD+18]

    Baldoni Roberto, Coppa Emilio, D'elia Daniele Cono, Demetrescu Camil, Finocchi Irene (2018) A survey of symbolic execution techniques. ACM Computing Surveys 51(3)

  5. [BDP15]

    Braione Pietro, Denaro Giovanni, Pezzè Mauro (2015) Symbolic execution of programs with heap inputs. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015), pp 602–613

  6. [BK94]

    Bonsangue Marcello, M., Kok Joost, N.: The weakest precondition calculus: Recursion and duality. Formal Aspect of Computing 6(1), 788–800 (1994)

    Article  Google Scholar 

  7. [CDE08]

    Cadar Cristian, Dunbar Daniel, Engler Dawson (2008) 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). USENIX Association, pp 209–224

  8. [CFS09]

    Chandra Satish, Fink Stephen J, Sridharan Manu (2009) Snugglebug: a powerful approach to weakest preconditions. In: Hind Michael, Diwan Amer (eds.), Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2009). ACM, pp 363–374

  9. [CGP+08]

    Cadar Cristian, Ganesh Vijay, Pawlowski Peter M, Dill David L, Engler Dawson R (2008) Exe: Automatically generating inputs of death. ACM Transactions on Information and System Security 12(2):10:1–10:38

  10. [dB99]

    de Boer Frank S (1999) A wp-calculus for OO. In: Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp 135–149

  11. [dBB19]

    de Boer Frank S, Bonsangue Marcello (2019) On the nature of symbolic execution. In: ter Beek Maurice H, McIver Annabelle, Oliveira José N (eds.) Formal Methods – The Next 30 Years, Lecture Notes in Computer Science. Springer, pp 64–80

  12. [dBBJ+20]

    de Boer Frank, Bonsangue Marcello, Johnsen Einar Broch, Pun Violet Ka I, Tarifa S Lizeth Tapia, Tveito Lars, : Sympaths: Symbolic execution meets partial order reduction. In: Bubel, R., Hähnle, R., et al. (eds.) Deductive Verification: The Next 70 Years. Springer (2020)

  13. [dBCJ07]

    de Boer Frank S, Clarke Dave, Johnsen Einar Broch (2007) A complete guide to the future. In: De Nicola Rocco (ed.), Proceedings of the 16th European Symposium on Programming Languages and Systems (ESOP 2007), volume 4421 of Lecture Notes in Computer Science, pp 316–330. Springer

  14. [DLR06]

    Deng Xianghua, Lee Jooyong, and Robby (2006) 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). IEEE Computer Society, pp 157–166

  15. [EGL09]

    Elkarablieh Bassem, Godefroid Patrice, Levin Michael Y (2009)Precise pointer reasoning for dynamic test generation. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis (ISSTA 2009). ACM, pp 129–140

  16. [FLP17]

    Aymeric, Fromherz, Luckow Kasper, S., Păsăreanu Corina, S.: Symbolic arrays in symbolic pathfinder. SIGSOFT Softw. Eng. Notes 41(6), 1–5 (2017)

    Google Scholar 

  17. [GKS05]

    Godefroid Patrice, Klarlund Nils, Sen Koushik (2005) DART: directed automated random testing. In: Sarkar Vivek, Hall Mary W (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005). ACM, pp 213–223

  18. [Gri81]

    Gries David (1981) The Science of Programming. Texts and Monographs in Computer Science. Springer

  19. [JHS+12]

    Broch, Johnsen Einar, Reiner, Hähnle, Jan, Schäfer, Rudolf, Schlatte, Martin, Steffen: ABS: A core language for abstract behavioral specification. In: Aichernig Bernhard, K., de Boer, Frank S., Bonsangue Marcello, M. (eds.) Formal Methods for Components and Objects - 9th International Symposium (FMCO 2010). Lecture Notes in Computer Science, vol. 6957, pp. 142–164. Springer (2012)

    Google Scholar 

  20. [KC19]

    Timotej, Kapus, Cristian, Cadar: A segmented memory model for symbolic execution. Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2019, 774–784 (2019)

    Google Scholar 

  21. [Kin76]

    King James, C.: Symbolic execution and program testing. Communications of ACM 19(7), 385–39 (1976)

    MathSciNet  Article  Google Scholar 

  22. [LRA17]

    Dorel, Lucanu, Vlad, Rusu, Andrei, Arusoaie: A generic framework for symbolic execution. Journal of Symbolic Computation 80(1), 125–163 (2017)

    MathSciNet  MATH  Google Scholar 

  23. [PMZC17]

    Perry David M, Mattavelli Andrea, Zhang Xiangyu, Cadar Cristian (2017) Accelerating array constraints in symbolic execution. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017). ACM, pp 68–78

  24. [SAB10]

    Schwartz Edward J, Avgerinos Thanassis, Brumley David (2010) All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: Proceedings of the 2010 IEEE Symposium on Security and Privacy, SP '10, page 317–331, USA, 2010. IEEE Computer Society

  25. [TS14]

    Trtík Marek, Strejček Jan (2014) Symbolic memory with pointers. In: Cassez Franck, Raskin Jean-François (eds.) Proc. Symp. on Automated Technology for Verification and Analysis (ATVA 2014), volume 8837 of Lecture Notes in Computer Science. Springer, pp 380–395

  26. [XMSN05]

    Xie Tao, Marinov Darko, Schulte Wolfram, Notkin David (2005) Symstra: A framework for generating object-oriented unit tests using symbolic execution. In: Proceeding of the international conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of Lecture Notes in Computer Science. Springer, pp 365–381

Download references

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.

Author information

Affiliations

Authors

Corresponding author

Correspondence to Frank S. de Boer.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Annabelle Mclver

Rights and permissions

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit https://creativecommons.org/licenses/by/4.0/.

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

de Boer, F.S., Bonsangue, M. Symbolic execution formally explained. Form Asp Comp (2021). https://doi.org/10.1007/s00165-020-00527-y

Download citation