{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T15:58:42Z","timestamp":1782316722666,"version":"3.54.5"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,2,2]],"date-time":"2021-02-02T00:00:00Z","timestamp":1612224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-020-00527-y","type":"journal-article","created":{"date-parts":[[2021,2,18]],"date-time":"2021-02-18T21:44:51Z","timestamp":1613684691000},"page":"617-636","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Symbolic execution formally explained"],"prefix":"10.1145","volume":"33","author":[{"given":"Frank S.","family":"de Boer","sequence":"first","affiliation":[{"name":"Centrum Wiskunde and Informatica (CWI), Leiden, The Netherlands"},{"name":"Leiden Institute Of Advanced Computer Science (LIACS), Leiden University, Leiden, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcello","family":"Bonsangue","sequence":"additional","affiliation":[{"name":"Leiden Institute Of Advanced Computer Science (LIACS), Leiden University, Leiden, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Albert Elvira Arenas Puri G\u00f3mez-Zamalloa Miguel Rojas Jos\u00e9\u00a0Miguel (2014) Test case generation by symbolic execution: Basic concepts a clp-based instance and actor-based concurrency. In: Marco Bernardo Ferruccio Damiani Reiner H\u00e4hnle Einar\u00a0Broch 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\u2013309","DOI":"10.1007\/978-3-319-07317-0_7"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Ahrendt Wolfgang Beckert Bernhard Bubel Richard H\u00e4hnle Reiner Schmitt Peter\u00a0H Ulbrich Mattias (eds.) (2016) Deductive Software Verification - The KeY Book - From Theory to Practice volume 10001 of Lecture Notes in Computer Science. Springer","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Apt Krzysztof\u00a0R de\u00a0Boer Frank Olderog Ernst-Rdiger (2009)Verification of Sequential and Concurrent Programs 3rd edition. Springer","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Baldoni Roberto Coppa Emilio D'elia Daniele\u00a0Cono Demetrescu Camil Finocchi Irene (2018) A survey of symbolic execution techniques. ACM Computing Surveys 51(3)","DOI":"10.1145\/3182657"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Braione Pietro Denaro Giovanni Pezz\u00e8 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\u2013613","DOI":"10.1145\/2786805.2786842"},{"issue":"1","key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"788","DOI":"10.1007\/BF01213603","article-title":"The weakest precondition calculus: Recursion and duality","volume":"6","author":"Bonsangue Marcello M","year":"1994","journal-title":"Formal Aspect of Computing"},{"key":"e_1_2_1_2_7_2","unstructured":"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\u2013224"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chandra Satish Fink Stephen\u00a0J 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\u2013374","DOI":"10.1145\/1543135.1542517"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cadar Cristian Ganesh Vijay Pawlowski Peter\u00a0M Dill David\u00a0L Engler Dawson\u00a0R (2008) Exe: Automatically generating inputs of death. ACM Transactions on Information and System Security 12(2):10:1\u201310:38","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_2_1_2_10_2","unstructured":"de\u00a0Boer Frank\u00a0S (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\u2013149"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"de\u00a0Boer Frank\u00a0S Bonsangue Marcello (2019) On the nature of symbolic execution. In: ter Beek Maurice\u00a0H McIver Annabelle Oliveira Jos\u00e9\u00a0N (eds.) Formal Methods \u2013 The Next 30 Years Lecture Notes in Computer Science. Springer pp 64\u201380","DOI":"10.1007\/978-3-030-30942-8_6"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"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\u00e4hnle R. et al. (eds.) Deductive Verification: The Next 70 Years. Springer (2020)","DOI":"10.1007\/978-3-030-64354-6_13"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"de\u00a0Boer Frank\u00a0S Clarke Dave Johnsen Einar\u00a0Broch (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\u2013330. Springer","DOI":"10.1007\/978-3-540-71316-6_22"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"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\u2013166","DOI":"10.1109\/ASE.2006.26"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Elkarablieh Bassem Godefroid Patrice Levin Michael\u00a0Y (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\u2013140","DOI":"10.1145\/1572272.1572288"},{"issue":"6","key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3011286.3011296","article-title":"Symbolic arrays in symbolic pathfinder","volume":"41","author":"Aymeric Fromherz","year":"2017","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Godefroid Patrice Klarlund Nils Sen Koushik (2005) DART: directed automated random testing. In: Sarkar Vivek Hall Mary\u00a0W (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005). ACM pp 213\u2013223","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Gries David (1981) The Science of Programming. Texts and Monographs in Computer Science. Springer","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_2_1_2_19_2","first-page":"142","volume-title":"Formal Methods for Components and Objects - 9th International Symposium (FMCO 2010)","author":"Broch Johnsen Einar","year":"2012"},{"key":"e_1_2_1_2_20_2","first-page":"774","article-title":"A segmented memory model for symbolic execution","volume":"2019","author":"Timotej Kapus","year":"2019","journal-title":"Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE"},{"issue":"7","key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King James C","year":"1976","journal-title":"Communications of ACM"},{"issue":"1","key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.jsc.2016.07.012","article-title":"A generic framework for symbolic execution","volume":"80","author":"Dorel Lucanu","year":"2017","journal-title":"Journal of Symbolic Computation"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Perry David\u00a0M 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\u201378","DOI":"10.1145\/3092703.3092728"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Schwartz Edward\u00a0J 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\u2013331 USA 2010. IEEE Computer Society","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Trt\u00edk Marek Strej\u010dek Jan (2014) Symbolic memory with pointers. In: Cassez Franck Raskin Jean-Fran\u00e7ois (eds.) Proc. Symp. on Automated Technology for Verification and Analysis (ATVA 2014) volume 8837 of Lecture Notes in Computer Science. Springer pp 380\u2013395","DOI":"10.1007\/978-3-319-11936-6_27"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"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\u2013381","DOI":"10.1007\/978-3-540-31980-1_24"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00527-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-020-00527-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00527-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00527-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:22:49Z","timestamp":1641486169000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00527-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":26,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-020-00527-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00527-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"10 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}