Algorithm selection for Dynamic Symbolic Execution: a preliminary study

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review


Given a portfolio of algorithms, the goal of Algorithm Selection (AS) is to select the best algorithm(s) for a new, unseen problem instance. Dynamic Symbolic Execution (DSE) brings together concrete and symbolic execution to maximise the program coverage. DSE uses a constraint solver to solve the path conditions and generate new inputs to explore. In this paper we join these lines of research by introducing a model that combines DSE and AS approaches. The proposed AS/DSE model is a generic and flexible framework enabling the DSE engine to solve the path conditions it collects with a portfolio of different solvers, by exploiting and extending the well-known AS techniques that have been developed over the last decade. In this way, one can increase the coverage and sometimes even outperform the aggregate coverage achievable by running simultaneously all the solvers of the portfolio.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings
EditorsMaribel Fernández
Place of PublicationCham Switzerland
Number of pages18
ISBN (Electronic)9783030684464
ISBN (Print)9783030684457
Publication statusPublished - 2021
EventInternational Symposium on Logic-based Program Synthesis and Transformation 2020 - Bologna, Italy
Duration: 7 Sep 20209 Sep 2020
Conference number: 30th (Proceedings) (Website)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Symposium on Logic-based Program Synthesis and Transformation 2020
Abbreviated titleLOPSTR 2020
Internet address


  • Algorithm selection
  • Constraint solving
  • Dynamic symbolic execution
  • Portfolio solving
  • Software verification

Cite this