{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T16:33:32Z","timestamp":1779381212030,"version":"3.53.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>During program traversing, symbolic execution collects path conditions and feeds them to a constraint solver to obtain feasible solutions. However, complex path conditions, like nonlinear constraints, which widely appear in programs, are hard to be handled efficiently by the existing solvers. In this paper, we adapt the classical symbolic execution framework with a machine learning approach for constraint satisfaction. The approach samples and learns from different solutions to identify potentially feasible area. This sampling-learning style solving can be applied in different class of complex problems easily. Therefore, incorporating this approach, our framework, MLBSE, supports the symbolic execution of not only simple linear path conditions, but also nonlinear arithmetic operations, and even black-box function calls of library methods. Meanwhile, thanks to the theoretical foundation of the machine learning based approach, when the solver fails to solve a path condition, we can have an estimation of the confidence in the satisfiability (ECS) of the problem to give users insights about how the problem is analyzed and whether they could ultimately find a solution. We implement MLBSE on the basis of Symbolic Path Finder (SPF) into a fully automatic Java symbolic execution engine. Users can feed their code to MLBSE directly, which is very convenient to use. To evaluate its performance, 22 real case programs are used as the benchmarks for MLBSE to generate test cases, which involve a total number of 1042 methods that are full of nonlinear operations, floating-point arithmetic as well as native method calls. Experiment results show that the coverage achieved by MLBSE is much higher than the state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/s00165-021-00538-3","type":"journal-article","created":{"date-parts":[[2021,5,26]],"date-time":"2021-05-26T17:06:03Z","timestamp":1622048763000},"page":"301-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Machine learning steered symbolic execution framework for complex software code"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yongjuan","family":"Liang","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhunyi","family":"Xie","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hong","family":"Qian","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi-Qi","family":"Hu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yang","family":"Yu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, People\u2019s Republic of China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"issue":"8","key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","article-title":"An orchestrated survey of methodologies for automated software test case generation","volume":"86","author":"Saswat A","year":"2013","journal-title":"J Syst Softw"},{"key":"e_1_2_1_2_2_2","unstructured":"Apache Commons Math (2018) https:\/\/commons.apache.org\/"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Borges M Amorim MD Anand S Bushnell D P\u0103s\u0103reanu CS (2012) Symbolic execution with interval solving and meta-heuristic search. In: 2012 IEEE fifth international conference on software testing verification and validation (ICST). IEEE pp 111\u2013120","DOI":"10.1109\/ICST.2012.91"},{"issue":"6","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/390016.808445","article-title":"Select\u2013a formal system for testing and debugging programs by symbolic execution","volume":"10","author":"Boyer Robert S","year":"1975","journal-title":"ACM SigPlan Not"},{"issue":"1","key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/2480359.2429133","article-title":"Automatic detection of floating-point exceptions","volume":"48","author":"Barr Earl T","year":"2013","journal-title":"ACM SIGPLAN Not"},{"issue":"3","key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"635","DOI":"10.1016\/0092-8674(84)90343-X","article-title":"Precise identification of individual promoters for transcription of each strand of human mitochondrial DNA","volume":"36","author":"Chang David D","year":"1984","journal-title":"Cell"},{"key":"e_1_2_1_2_7_2","first-page":"209","article-title":"Klee: unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","author":"Cristian C","year":"2008","journal-title":"OSDI"},{"issue":"4","key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1080\/00031305.1995.10476177","article-title":"Understanding the metropolis-hastings algorithm","volume":"49","author":"Siddhartha C","year":"1995","journal-title":"Am Stat"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cadar C Godefroid P Khurshid S P\u0103s\u0103reanu CS Sen K Tillmann N Visser W (2011) Symbolic execution for software testing in practice: preliminary assessment. In: Proceedings of the 33rd international conference on software engineering. ACM pp 1066\u20131071","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","article-title":"A system to generate test data and symbolically execute programs","volume":"3","author":"Clarke Lori A","year":"1976","journal-title":"IEEE Trans Softw Eng"},{"key":"e_1_2_1_2_11_2","unstructured":"Cyclomatic Complexity (2018) http:\/\/eclemma.org\/jacoco\/trunk\/doc\/counters.html"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dinges P Agha G (2014) Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering. ACM pp 425\u2013436","DOI":"10.1145\/2635868.2635889"},{"issue":"3","key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1080\/00029890.1973.11993265","article-title":"Hilbert's tenth problem is unsolvable","volume":"80","author":"Martin D","year":"1973","journal-title":"Am Math Mon"},{"key":"e_1_2_1_2_14_2","first-page":"209","article-title":"Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure","volume":"1","author":"Martin F","year":"2007","journal-title":"J Satisf Boolean Model Comput"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Fu Zhoulai S. Zhendong : Xsat: a fast floating-point satisfiability solver. In: Chaudhuri S. Farzan A. (eds.) Computer aided verification pp. 187\u2013209. Springer Cham (2016)","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Galeotti JP Fraser G Arcuri A (2013) Improving search-based test suite generation with dynamic symbolic execution. In: 2013 IEEE 24th international symposium on software reliability engineering (ISSRE). IEEE pp 360\u2013369","DOI":"10.1109\/ISSRE.2013.6698889"},{"issue":"6","key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1064978.1065036","article-title":"Dart: directed automated random testing","volume":"40","author":"Patrice G","year":"2005","journal-title":"ACM Sigplan Not"},{"issue":"4","key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1287\/inte.20.4.74","article-title":"Tabu search: a tutorial","volume":"20","author":"Fred G","year":"1990","journal-title":"Interfaces"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/1538674"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Gies D Rahmat-samii Y (2004) Particle swarm optimization (pso) for reflector antenna shaping. In: Antennas and propagation society international symposium 2004. IEEE vol 3 pp 2289\u20132292","DOI":"10.1109\/APS.2004.1331828"},{"issue":"4","key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model checking java programs using java pathfinder","volume":"2","author":"Klaus H","year":"2000","journal-title":"Int J Softw Tools Technol Transf"},{"key":"e_1_2_1_2_22_2","unstructured":"Jacoco (2018) http:\/\/www.eclemma.org\/jacoco\/"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"issue":"7","key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"Kingl James C","year":"1976","journal-title":"Commun ACM"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Luckow K Dimja\u0161evi\u0107 M Giannakopoulou D Howar F Isberner M Kahsai T Rakamari\u0107 Z Raman V (2016) JDart: a dynamic symbolic analysis framework. In: Chechik M Raskin J-F (eds) Proceedings of the 22nd international conference on tools and algorithms for the construction and analysis of systems (TACAS) lecture notes in computer science vol 9636. Springer Berlin pp 442\u2013459","DOI":"10.1007\/978-3-662-49674-9_26"},{"issue":"1","key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF02473201","article-title":"Improving structural integrity of cryosections for immunogold labeling","volume":"106","author":"Willisa L","year":"1996","journal-title":"Histochem Cell Biol"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Li X Liang Y Qian H Hu Y-Q Bu L Yu Y Chen X Li X (2016) Symbolic execution of complex program driven by machine learning based constraint solving. In: Lo D Apel S Khurshid S (eds) Proceedings of the 31st IEEE\/ACM international conference on automated software engineering ASE 2016 Singapore September 3\u20137 2016. ACM pp 554\u2013559","DOI":"10.1145\/2970276.2970364"},{"issue":"2","key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1002\/stvr.294","article-title":"Search-based software test data generation: a survey","volume":"14","author":"Phil MM","year":"2004","journal-title":"Softw Test Verif Reliab"},{"key":"e_1_2_1_2_29_2","unstructured":"Minizinc (2018) http:\/\/www.minizinc.org\/"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1561\/2200000038"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu CS Rungta N (2010) Symbolic pathfinder: symbolic execution of java bytecode. In: Proceedings of the IEEE\/ACM international conference on automated software engineering. ACM pp 179\u2013180","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_2_32_2","volume-title":"Numerical recipes: the art of scientific computing","author":"Press William H","year":"2007","edition":"3"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu CS Rungta N Visser W (2011) Symbolic execution with mixed concrete-symbolic solving. In: Proceedings of the 2011 international symposium on software testing and analysis. ACM pp 34\u201344","DOI":"10.1145\/2001420.2001425"},{"issue":"4","key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","article-title":"A survey of new trends in symbolic execution for software testing and analysis","volume":"11","author":"P\u0103s\u0103reanu Corina S","year":"2009","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"3","key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/s10515-013-0122-2","article-title":"Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis","volume":"20","author":"P\u0103s\u0103reanu Corina S","year":"2013","journal-title":"Autom Softw Eng"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Qian H Yu Y (2016) On sampling-and-classification optimization in discrete domains. In: Proceedings of the 2016 IEEE congress on evolutionary computation (CEC'16) Vancouver Canada pp 4374\u20134381","DOI":"10.1109\/CEC.2016.7744346"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer aided verification","author":"Sen K","year":"2006"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Shafiei N van Breugel F (2014) Automatic handling of native methods in java pathfinder. In: Proceedings of the 2014 international SPIN symposium on model checking of software. ACM pp 97\u2013100","DOI":"10.1145\/2632362.2632363"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"},{"key":"e_1_2_1_2_40_2","unstructured":"Scientific Computation (2018) https:\/\/github.com\/elizabethzhenliu\/ScientificComputation"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Sen K (2007) Concolic testing. In: Proceedings of the twenty-second IEEE\/ACM international conference on automated software engineering. ACM pp 571\u2013572","DOI":"10.1145\/1321631.1321746"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Bobak S. Kevin S. Ziyu W. Adams Ryan P. de Freitas Nando : Taking the human out of the loop: a review of Bayesian optimization. Proc IEEE 104 (1) 148\u2013175 (2016)","DOI":"10.1109\/JPROC.2015.2494218"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Tillmann N De Halleux J (2008) Pex\u2013white box test generation for. net. In: Tests and proofs. Springer Berlin pp 134\u2013153","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Yu Y Qian H Hu Y-Q (2016) Derivative-free optimization via classification. In: Proceedings of the 30th AAAI conference on artificial intelligence (AAAI'16) Phoenix AZ","DOI":"10.1609\/aaai.v30i1.10289"},{"key":"e_1_2_1_2_45_2","unstructured":"Yu Y Hu Y-Q Qian H (2017) Sequential classification-based optimization for direct policy search. In: Proceedings of the 31st AAAI conference on artificial intelligence (AAAI'17) San Francisco CA pp 2029\u20132035"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00538-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00538-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00538-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00538-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,31]],"date-time":"2024-08-31T16:13:16Z","timestamp":1725120796000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00538-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["10.1007\/s00165-021-00538-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00538-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"10 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 November 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}