pith. sign in

arxiv: 1907.09700 · v1 · pith:SXNWFKHEnew · submitted 2019-07-23 · 💻 cs.SE

Enhancing Dynamic Symbolic Execution by Automatically Learning Search Heuristics

Pith reviewed 2026-05-24 17:39 UTC · model grok-4.3

classification 💻 cs.SE
keywords dynamic symbolic executionsearch heuristicsparametric optimizationcode coveragebug findingpath explorationKLEE
0
0 comments X

The pith

Automatically learned parametric search heuristics for dynamic symbolic execution outperform manually designed ones in branch coverage and bug finding.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks to replace manual design of path-selection strategies in dynamic symbolic execution with an automated process that tunes a parametric form of heuristic for each target program. It shows that an efficient search over the parameter space can locate settings yielding higher coverage than standard hand-crafted heuristics when evaluated inside industrial tools such as KLEE. A sympathetic reader would care because manual heuristics are described as difficult to create and frequently suboptimal or unstable across programs; replacing that step with per-program optimization could therefore raise the practical effectiveness of symbolic execution under fixed time budgets. The central move is to treat the heuristic itself as a learnable object rather than a fixed artifact.

Core claim

We define a class of parametric search heuristics and present an algorithm that efficiently finds an optimal heuristic for each subject program. Experimental results with industrial-strength symbolic execution tools show that the generated heuristics significantly outperform existing manually-crafted heuristics in terms of branch coverage and bug-finding.

What carries the argument

A parametric search heuristic whose parameters are optimized by a dedicated learning algorithm to maximize coverage on a given program.

If this is right

  • Higher branch coverage is achieved within the same time budget.
  • More bugs are discovered during the execution runs.
  • Search behavior becomes tuned to the specific program rather than relying on a single general-purpose rule.
  • The manual effort required to craft and maintain heuristics across different programs is reduced.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same learning loop could be applied to other search-based analyses that currently depend on hand-tuned priority functions.
  • Retraining the parameters on new versions of a program might be needed if code changes alter the optimal exploration order.
  • The approach opens the possibility of comparing learned heuristics across families of similar programs to identify transferable parameter patterns.

Load-bearing premise

The parametric form chosen for the heuristics is expressive enough to contain near-optimal strategies for the subject programs.

What would settle it

A head-to-head experiment on held-out programs in which the learned heuristic produces no higher branch coverage on average than the strongest existing manual heuristic.

Figures

Figures reproduced from arXiv: 1907.09700 by Hakjoo Oh, Jingyoung Kim, Junhee Lee, Seongjoon Hong, Sooyoung Cha.

Figure 1
Figure 1. Figure 1: Limitations of existing search heuristics for concolic testing: No search heuristic performs well consistently. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Limitations of existing search heuristics for execution-generated testing (KLEE) [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Average branch coverage achieved by each search heuristic on 6 large benchmarks for concolic testing [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Performance w.r.t. execution time (vim-5.7) [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Average branch coverage achieved by top 6 search heuristics on 6 large benchmarks for execution-generated testing [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Average coverage of each search heuristic for concolic testing on multiple subsequent program variants [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Average coverage of each search heuristic for execution-generated testing on multiple subsequent program variants [PITH_FULL_IMAGE:figures/full_fig_p014_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Comparison of our learning algorithm and random sampling method [PITH_FULL_IMAGE:figures/full_fig_p015_8.png] view at source ↗
read the original abstract

We present a technique to automatically generate search heuristics for dynamic symbolic execution. A key challenge in dynamic symbolic execution is how to effectively explore the program's execution paths to achieve high code coverage in a limited time budget. Dynamic symbolic execution employs a search heuristic to address this challenge, which favors exploring particular types of paths that are most likely to maximize the final coverage. However, manually designing a good search heuristic is nontrivial and typically ends up with suboptimal and unstable outcomes. The goal of this paper is to overcome this shortcoming of dynamic symbolic execution by automatically learning search heuristics. We define a class of search heuristics, namely a parametric search heuristic, and present an algorithm that efficiently finds an optimal heuristic for each subject program. Experimental results with industrial-strength symbolic execution tools (e.g., KLEE) show that our technique can successfully generate search heuristics that significantly outperform existing manually-crafted heuristics in terms of branch coverage and bug-finding.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims to automatically generate effective search heuristics for dynamic symbolic execution (DSE) by defining a parametric class of heuristics and presenting an algorithm that optimizes parameters per subject program. Experiments using industrial tools such as KLEE are said to show that the learned heuristics significantly outperform manually crafted ones on branch coverage and bug-finding.

Significance. If the results are robust to the overfitting risks inherent in per-program optimization, the approach could meaningfully reduce the manual effort in tuning DSE tools and improve their practical effectiveness for software testing.

major comments (2)
  1. [§5] §5 (Experimental Evaluation): the central empirical claim of outperformance lacks any description of held-out validation sets, multiple random seeds for the learning procedure, or variance across independent runs; without these, the per-program parameter search on the same traces used for final reporting risks producing inflated coverage numbers that do not generalize.
  2. [§4] §4 (Learning Algorithm): no expressiveness argument or bound is given showing that the chosen parametric family is rich enough to contain near-optimal heuristics for the evaluated programs, leaving open the possibility that reported gains are artifacts of the specific parameterization rather than a general advance.
minor comments (1)
  1. [Abstract] Abstract: asserts 'significantly outperform' without any quantitative numbers, protocol details, or subject-program counts, making it impossible to gauge the magnitude of the claimed improvement from the summary alone.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the two major comments below, acknowledging where the manuscript is currently limited and outlining planned revisions.

read point-by-point responses
  1. Referee: §5 (Experimental Evaluation): the central empirical claim of outperformance lacks any description of held-out validation sets, multiple random seeds for the learning procedure, or variance across independent runs; without these, the per-program parameter search on the same traces used for final reporting risks producing inflated coverage numbers that do not generalize.

    Authors: We agree this is a valid concern. The current evaluation optimizes and reports on the same program traces without held-out sets or multi-seed variance, which limits claims of robustness. In the revision we will rerun the learning procedure with multiple random seeds, report mean and variance of branch coverage and bug-finding results, and add a discussion of overfitting risks and how per-program optimization is meant to be applied in practice. revision: yes

  2. Referee: §4 (Learning Algorithm): no expressiveness argument or bound is given showing that the chosen parametric family is rich enough to contain near-optimal heuristics for the evaluated programs, leaving open the possibility that reported gains are artifacts of the specific parameterization rather than a general advance.

    Authors: The parametric family was constructed to subsume several standard hand-crafted heuristics (e.g., random, coverage-guided) as special cases, which is why we expected it to be sufficiently expressive. However, no formal expressiveness argument or bound was provided. We will add a subsection discussing the design rationale and empirical evidence that the family recovers or improves upon known good heuristics on the evaluated subjects; a general theoretical bound is beyond the scope of this work but we will clarify the intended scope. revision: partial

Circularity Check

0 steps flagged

No circularity; empirical learning and evaluation are independent

full rationale

The paper defines a parametric class of search heuristics, presents an optimization algorithm to select parameters per program, and reports experimental coverage/bug-finding results on KLEE. No equations, predictions, or uniqueness claims reduce by construction to fitted inputs or self-citations. The central claim is an empirical comparison whose validity rests on held-out test runs rather than any definitional equivalence. No load-bearing self-citation chains or ansatz smuggling appear in the abstract or described method.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, axioms, or invented entities; the technique implicitly assumes that a parametric family exists and that optimization is tractable, but these are not enumerated.

pith-pipeline@v0.9.0 · 5692 in / 999 out tokens · 24773 ms · 2026-05-24T17:39:44.070190+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

70 extracted references · 70 canonical work pages

  1. [1]

    CUTE: A concolic unit testing engine for C,

    K. Sen, D. Marinov, and G. Agha, “CUTE: A concolic unit testing engine for C,” in Proceedings of the 10th European Software Engineer- ing Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering , ser. ESEC/FSE ’05, 2005, pp. 263–272

  2. [2]

    DART: Directed auto- mated random testing,

    P . Godefroid, N. Klarlund, and K. Sen, “DART: Directed auto- mated random testing,” in Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’05, 2005, pp. 213–223

  3. [3]

    Execution generated test cases: How to make systems code crash itself,

    C. Cadar and D. Engler, “Execution generated test cases: How to make systems code crash itself,” in Proceedings of the 12th International Conference on Model Checking Software , ser. SPIN’05, 2005, pp. 2–23

  4. [4]

    EXE: Automatically generating inputs of death,

    C. Cadar, V . Ganesh, P . M. Pawlowski, D. L. Dill, and D. R. Engler, “EXE: Automatically generating inputs of death,” in Proceedings of the 13th ACM Conference on Computer and Communications Security , ser. CCS ’06, 2006, pp. 322–335

  5. [5]

    Enhancing symbolic execution with veritesting,

    T. Avgerinos, A. Rebert, S. K. Cha, and D. Brumley, “Enhancing symbolic execution with veritesting,” in Proceedings of the 36th International Conference on Software Engineering, ser. ICSE ’14, 2014, pp. 1083–1094

  6. [6]

    Guiding dynamic symbolic execution toward unverified program executions,

    M. Christakis, P . M ¨uller, and V . W ¨ustholz, “Guiding dynamic symbolic execution toward unverified program executions,” in Proceedings of the 38th International Conference on Software Engineer- ing, ser. ICSE ’16, 2016, pp. 144–155

  7. [7]

    Regular property guided dynamic symbolic execution,

    Y. Zhang, Z. Clien, J. Wang, W. Dong, and Z. Liu, “Regular property guided dynamic symbolic execution,” in Proceedings of the 37th International Conference on Software Engineering - Volume 1 , ser. ICSE ’15, 2015, pp. 643–653

  8. [8]

    CAB- Fuzz: Practical concolic testing techniques for COTS operating sys- tems,

    S. Y. Kim, S. Lee, I. Yun, W. Xu, B. Lee, Y. Yun, and T. Kim, “CAB- Fuzz: Practical concolic testing techniques for COTS operating sys- tems,” in 2017 USENIX Annual Technical Conference , ser. USENIX ATC ’17, 2017, pp. 689–701

  9. [9]

    Driller: Augmenting fuzzing through selective symbolic execution,

    N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna, “Driller: Augmenting fuzzing through selective symbolic execution,” in Proceedings of the Symposium on Network and Distributed System Security , ser. NDSS ’16, 2016, pp. 1–16

  10. [10]

    SymCerts: Practical symbolic execution for exposing noncompliance in x.509 certificate validation implemen- tations,

    S. Y. Chau, O. Chowdhury, E. Hoque, H. Ge, A. Kate, C. Nita- Rotaru, and N. Li, “SymCerts: Practical symbolic execution for exposing noncompliance in x.509 certificate validation implemen- tations,” in 2017 IEEE Symposium on Security and Privacy , ser. S&P ’17, 2017, pp. 503–520

  11. [11]

    FirmUSB: Vetting usb device firmware using domain informed symbolic execution,

    G. Hernandez, F. Fowze, D. J. Tian, T. Yavuz, and K. R. Butler, “FirmUSB: Vetting usb device firmware using domain informed symbolic execution,” in Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security , ser. CCS ’17, 2017, pp. 2245–2262

  12. [12]

    Inception: System-wide security testing of real-world embedded systems software,

    N. Corteggiani, G. Camurati, and A. Francillon, “Inception: System-wide security testing of real-world embedded systems software,” in 27th USENIX Security Symposium , ser. USENIX Se- curity ’18, 2018, pp. 309–326

  13. [13]

    Concolic testing for deep neural networks,

    Y. Sun, M. Wu, W. Ruan, X. Huang, M. Kwiatkowska, and D. Kroening, “Concolic testing for deep neural networks,” in Pro- ceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ser. ASE ’18, 2018, pp. 109–119

  14. [14]

    DeepConcolic: Testing and debugging deep neural networks,

    Y. Sun, X. Huang, D. Kroening, J. Sharp, M. Hill, and R. Ashmore, “DeepConcolic: Testing and debugging deep neural networks,” in Proceedings of the 41st International Conference on Software Engineer- ing: Companion Proceedings, ser. ICSE ’19, 2019, pp. 111–114

  15. [15]

    A new approach to program testing,

    J. C. King, “A new approach to program testing,” SIGPLAN Not., pp. 228–233, 1975

  16. [16]

    Symbolic execution and program testing,

    ——, “Symbolic execution and program testing,” Commun. ACM, pp. 385–394, 1976

  17. [17]

    SELECT–a formal system for testing and debugging programs by symbolic execution,

    R. S. Boyer, B. Elspas, and K. N. Levitt, “SELECT–a formal system for testing and debugging programs by symbolic execution,” SIGPLAN Not., pp. 234–245, 1975

  18. [18]

    Symbolic testing and the dissect symbolic evalu- ation system,

    W. E. Howden, “Symbolic testing and the dissect symbolic evalu- ation system,” IEEE Transactions on Software Engineering , pp. 266– 278, 1977

  19. [19]

    Symbolic execution for software testing: Three decades later,

    C. Cadar and K. Sen, “Symbolic execution for software testing: Three decades later,” Commun. ACM, pp. 82–90, 2013

  20. [20]

    Heuristics for scalable dynamic test gener- ation,

    J. Burnim and K. Sen, “Heuristics for scalable dynamic test gener- ation,” in Proceedings of 23rd IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’08, 2008, pp. 443–446

  21. [21]

    Automated white- box fuzz testing,

    P . Godefroid, M. Y. Levin, and D. A. Molnar, “Automated white- box fuzz testing,” in Proceedings of the Symposium on Network and Distributed System Security, ser. NDSS ’08, 2008, pp. 151–166

  22. [22]

    KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs,

    C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs,” in Proceedings of the 8th USENIX Conference on Oper- ating Systems Design and Implementation , ser. OSDI ’08, 2008, pp. 209–224

  23. [23]

    How we get there: A context-guided search strategy in concolic testing,

    H. Seo and S. Kim, “How we get there: A context-guided search strategy in concolic testing,” in Proceedings of the 22nd ACM SIG- SOFT International Symposium on Foundations of Software Engineer- ing, ser. FSE ’14, 2014, pp. 413–424

  24. [24]

    CarFast: Achieving higher statement coverage faster,

    S. Park, B. M. M. Hossain, I. Hussain, C. Csallner, M. Grechanik, K. Taneja, C. Fu, and Q. Xie, “CarFast: Achieving higher statement coverage faster,” in Proceedings of the ACM SIGSOFT 20th Interna- tional Symposium on the Foundations of Software Engineering, ser. FSE ’12, 2012, pp. 35:1–35:11

  25. [25]

    Steering symbolic execution to less traveled paths,

    Y. Li, Z. Su, L. Wang, and X. Li, “Steering symbolic execution to less traveled paths,” in Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages, and Applications, ser. OOPSLA ’13, 2013, pp. 19–32

  26. [26]

    Automatically generating search heuristics for concolic testing,

    S. Cha, S. Hong, J. Lee, and H. Oh, “Automatically generating search heuristics for concolic testing,” in Proceedings of the 40th International Conference on Software Engineering, ser. ICSE ’18, 2018, pp. 1244–1254

  27. [27]

    Industrial application of concolic testing approach: A case study on libexif by using crest- bv and klee,

    Y. Kim, M. Kim, Y. Kim, and Y. Jang, “Industrial application of concolic testing approach: A case study on libexif by using crest- bv and klee,” in Proceedings of the 34th International Conference on Software Engineering, ser. ICSE ’12, 2012, pp. 1143–1152

  28. [28]

    A survey of symbolic execution techniques,

    R. Baldoni, E. Coppa, D. C. D’elia, C. Demetrescu, and I. Finocchi, “A survey of symbolic execution techniques,” ACM Comput. Surv., pp. 50:1–50:39, 2018

  29. [29]

    Parallel symbolic execution for automated real-world software testing,

    S. Bucur, V . Ureche, C. Zamfir, and G. Candea, “Parallel symbolic execution for automated real-world software testing,” in Proceed- ings of the Sixth Conference on Computer Systems , ser. EuroSys ’11, 2011, pp. 183–198

  30. [30]

    DASE: Document- assisted symbolic execution for improving automated software testing,

    E. Wong, L. Zhang, S. Wang, T. Liu, and L. Tan, “DASE: Document- assisted symbolic execution for improving automated software testing,” in Proceedings of the 37th International Conference on Soft- ware Engineering - Volume 1, ser. ICSE ’15, 2015, pp. 620–631

  31. [31]

    C. A. concolic test generation tool for C, https://github.com/ jburnim/crest, 2008

  32. [32]

    Feedback-directed unit test generation for c/c++ using concolic execution,

    P . Garg, F. Ivancic, G. Balakrishnan, N. Maeda, and A. Gupta, “Feedback-directed unit test generation for c/c++ using concolic execution,” in Proceedings of the 2013 International Conference on Software Engineering, ser. ICSE ’13, 2013, pp. 132–141

  33. [33]

    The S2E Platform: Design, implementation, and applications,

    V . Chipounov, V . Kuznetsov, and G. Candea, “The S2E Platform: Design, implementation, and applications,” ACM Trans. Comput. Syst., pp. 2:1–2:49, 2012

  34. [34]

    Make Test-zesti: A symbolic exe- cution solution for improving regression testing,

    P . D. Marinescu and C. Cadar, “Make Test-zesti: A symbolic exe- cution solution for improving regression testing,” in Proceedings of the 34th International Conference on Software Engineering , ser. ICSE ’12, 2012, pp. 716–726. 19

  35. [35]

    Post- conditioned symbolic execution,

    Q. Yi, Z. Yang, S. Guo, C. Wang, J. Liu, and C. Zhao, “Post- conditioned symbolic execution,” in 2015 IEEE 8th International Conference on Software Testing, Verification and Validation , ser. ICST ’15, 2015, pp. 1–10

  36. [36]

    Eliminating path redundancy via postconditioned symbolic execution,

    ——, “Eliminating path redundancy via postconditioned symbolic execution,” IEEE Trans. Softw. Eng., pp. 25–43, 2018

  37. [37]

    Efficient state merging in symbolic execution,

    V . Kuznetsov, J. Kinder, S. Bucur, and G. Candea, “Efficient state merging in symbolic execution,” in Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Imple- mentation, ser. PLDI ’12, 2012, pp. 193–204

  38. [38]

    Chopped symbolic execution,

    D. Trabish, A. Mattavelli, N. Rinetzky, and C. Cadar, “Chopped symbolic execution,” in Proceedings of the 40th International Confer- ence on Software Engineering, ser. ICSE ’18, 2018, pp. 350–360

  39. [39]

    Abstraction-driven concolic testing,

    P . Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” in Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583, ser. VMCAI ’16, 2016, pp. 328–347

  40. [40]

    SCORE: A scalable concolic testing tool for reliable embedded software,

    Y. Kim and M. Kim, “SCORE: A scalable concolic testing tool for reliable embedded software,” in Proceedings of the 19th ACM SIG- SOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ser. ESEC/FSE ’11, 2011, pp. 420–423

  41. [41]

    RWset: Attacking path explosion in constraint-based test generation,

    P . Boonstoppel, C. Cadar, and D. Engler, “RWset: Attacking path explosion in constraint-based test generation,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS ’08, 2008, pp. 351–366

  42. [42]

    Sym- bolic execution with existential second-order constraints,

    S. Mechtaev, A. Griggio, A. Cimatti, and A. Roychoudhury, “Sym- bolic execution with existential second-order constraints,” in Pro- ceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2018, 2018, pp. 389–399

  43. [43]

    Gnu Bug Report (gawk), http://gnu.utils.bug.narkive.com/ Udtl5IZR/gawk-bug, 2005

  44. [44]

    GNU Bug Report (grep), https://www.gnu.org/software/grep/ manual/html node/Reporting-Bugs.html, 2014

  45. [45]

    The yices smt solver,

    B. Dutertre and L. D. Moura, “The yices smt solver,” Tech. Rep., 2006

  46. [46]

    A decision procedure for bit-vectors and arrays,

    V . Ganesh and D. L. Dill, “A decision procedure for bit-vectors and arrays,” in International Conference on Computer Aided Verification , ser. CAV ’07, 2007, pp. 519–531

  47. [47]

    Fitness- guided path exploration in dynamic symbolic execution,

    T. Xie, N. Tillmann, J. de Halleux, and W. Schulte, “Fitness- guided path exploration in dynamic symbolic execution,” in 2009 IEEE/IFIP International Conference on Dependable Systems Networks , 2009, pp. 359–368

  48. [48]

    Hybrid concolic testing,

    R. Majumdar and K. Sen, “Hybrid concolic testing,” in Proceedings of the 29th International Conference on Software Engineering, ser. ICSE ’07, 2007, pp. 416–426

  49. [49]

    Improving structural testing of object- oriented programs via integrating evolutionary testing and sym- bolic execution,

    K. Inkumsah and T. Xie, “Improving structural testing of object- oriented programs via integrating evolutionary testing and sym- bolic execution,” in Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering , ser. ASE ’08, 2008, pp. 297–306

  50. [50]

    Improving function coverage with munch: A hybrid fuzzing and directed symbolic execution approach,

    S. Ognawala, T. Hutzelmann, E. Psallida, and A. Pretschner, “Improving function coverage with munch: A hybrid fuzzing and directed symbolic execution approach,” in Proceedings of the 33rd Annual ACM Symposium on Applied Computing , ser. SAC ’18, 2018, pp. 1475–1482

  51. [51]

    American Fuzzy Lop (AFL) Fuzzer, https://github.com/ mirrorer/afl, 2017

  52. [52]

    Boosting concolic testing via interpolation,

    J. Jaffar, V . Murali, and J. A. Navas, “Boosting concolic testing via interpolation,” in Proceedings of the 9th Joint Meeting on Foundations of Software Engineering, ser. ESEC/FSE ’13, 2013, pp. 48–58

  53. [53]

    Compositional dynamic test generation,

    P . Godefroid, “Compositional dynamic test generation,” in Pro- ceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’07, 2007, pp. 47–54

  54. [54]

    Com- positional may-must program analysis: Unleashing the power of alternation,

    P . Godefroid, A. V . Nori, S. K. Rajamani, and S. D. Tetali, “Com- positional may-must program analysis: Unleashing the power of alternation,” in Proceedings of the 37th Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages , ser. POPL ’10, 2010, pp. 43–56

  55. [55]

    Template-guided concolic testing via online learning,

    S. Cha, S. Lee, and H. Oh, “Template-guided concolic testing via online learning,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering , ser. ASE ’18, 2018, pp. 408–418

  56. [56]

    Boost symbolic execution using dynamic state merging and forking,

    C. Zhang, W. Yin, and Z. Lin, “Boost symbolic execution using dynamic state merging and forking,” in International Workshop on Quantitative Approaches to Software Quality, 2018, pp. 14–21

  57. [57]

    MultiSE: Multi-path symbolic execution using value summaries,

    K. Sen, G. Necula, L. Gong, and W. Choi, “MultiSE: Multi-path symbolic execution using value summaries,” in Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering , ser. ESEC/FSE ’15, 2015, pp. 842–853

  58. [58]

    Solving complex path conditions through heuristic search on induced polytopes,

    P . Dinges and G. Agha, “Solving complex path conditions through heuristic search on induced polytopes,” in Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. FSE ’14, 2014, pp. 425–436

  59. [59]

    Yet another local search method for constraint solving,

    P . Codognet and D. Diaz, “Yet another local search method for constraint solving,” in International Symposium on Stochastic Algo- rithms, 2001, pp. 73–90

  60. [60]

    Search-driven string constraint solving for vulnerability detection,

    J. Thom ´e, L. K. Shar, D. Bianculli, and L. Briand, “Search-driven string constraint solving for vulnerability detection,” in Proceed- ings of the 39th International Conference on Software Engineering , ser. ICSE ’17, 2017, pp. 198–208

  61. [61]

    Symbolic execution of complex program driven by ma- chine learning based constraint solving,

    X. Li, Y. Liang, H. Qian, Y.-Q. Hu, L. Bu, Y. Yu, X. Chen, and X. Li, “Symbolic execution of complex program driven by ma- chine learning based constraint solving,” in Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineer- ing, ser. ASE ’16, 2016, pp. 554–559

  62. [62]

    Accelerating array constraints in symbolic execution,

    D. M. Perry, A. Mattavelli, X. Zhang, and C. Cadar, “Accelerating array constraints in symbolic execution,” in Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA ’17, 2017, pp. 68–78

  63. [63]

    Learn&fuzz: Machine learning for input fuzzing,

    P . Godefroid, H. Peleg, and R. Singh, “Learn&fuzz: Machine learning for input fuzzing,” in Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’17, 2017, pp. 50–59

  64. [64]

    Skyfire: Data-driven seed generation for fuzzing,

    J. Wang, B. Chen, L. Wei, and Y. Liu, “Skyfire: Data-driven seed generation for fuzzing,” in 2017 IEEE Symposium on Security and Privacy, ser. S&P ’17, 2017, pp. 579–594

  65. [65]

    Qbe: Qlearning-based exploration of android applications,

    Y. Koroglu, A. Sen, O. Muslu, Y. Mete, C. Ulker, T. Tanriverdi, and Y. Donmez, “Qbe: Qlearning-based exploration of android applications,” in 2018 IEEE 11th International Conference on Software Testing, Verification and Validation, ser. ICST ’18, 2018, pp. 105–115

  66. [66]

    Guided gui testing of an- droid apps with minimal restart and approximate learning,

    W. Choi, G. Necula, and K. Sen, “Guided gui testing of an- droid apps with minimal restart and approximate learning,” in Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages, and Applications , ser. OOPSLA ’13, 2013, pp. 623–640

  67. [67]

    Reinforce- ment learning for automatic test case prioritization and selection in continuous integration,

    H. Spieker, A. Gotlieb, D. Marijan, and M. Mossige, “Reinforce- ment learning for automatic test case prioritization and selection in continuous integration,” in Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA ’17, 2017, pp. 12–22

  68. [68]

    An exploration of statistical models for automated test case generation,

    J. Sant, A. Souter, and L. Greenwald, “An exploration of statistical models for automated test case generation,” in Proceedings of the Third International Workshop on Dynamic Analysis , ser. WODA ’05, 2005, pp. 1–7

  69. [69]

    Search-based software testing: Past, present and future,

    P . McMinn, “Search-based software testing: Past, present and future,” in 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops, 2011, pp. 153–163

  70. [70]

    Search-based software engineering: Trends, techniques and applications,

    M. Harman, S. A. Mansouri, and Y. Zhang, “Search-based software engineering: Trends, techniques and applications,” ACM Comput. Surv., pp. 11:1–11:61, 2012