Algorithm selection for Dynamic Symbolic Execution: a preliminary study

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

doi:10.1007/978-3-030-68446-4_10

Algorithm selection for Dynamic Symbolic Execution: a preliminary study

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

Department of Data Science & AI

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

1 Citation (Scopus)

Abstract

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 language	English
Title of host publication	Logic-Based Program Synthesis and Transformation
Subtitle of host publication	30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings
Editors	Maribel Fernández
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	192-209
Number of pages	18
ISBN (Electronic)	9783030684464
ISBN (Print)	9783030684457
DOIs	https://doi.org/10.1007/978-3-030-68446-4_10
Publication status	Published - 2021
Event	International Symposium on Logic-based Program Synthesis and Transformation 2020 - Bologna, Italy Duration: 7 Sept 2020 → 9 Sept 2020 Conference number: 30th https://link.springer.com/book/10.1007/978-3-030-68446-4 (Proceedings) https://nms.kcl.ac.uk/maribel.fernandez/LOPSTR2020/ (Website)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12561
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Symposium on Logic-based Program Synthesis and Transformation 2020
Abbreviated title	LOPSTR 2020
Country/Territory	Italy
City	Bologna
Period	7/09/20 → 9/09/20
Internet address	https://link.springer.com/book/10.1007/978-3-030-68446-4 (Proceedings) https://nms.kcl.ac.uk/maribel.fernandez/LOPSTR2020/ (Website)

Keywords

Algorithm selection
Constraint solving
Dynamic symbolic execution
Portfolio solving
Software verification

Access to Document

10.1007/978-3-030-68446-4_10

Cite this

Amadini, R., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2021). Algorithm selection for Dynamic Symbolic Execution: a preliminary study. In M. Fernández (Ed.), Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings (pp. 192-209). (Lecture Notes in Computer Science ; Vol. 12561). Springer. https://doi.org/10.1007/978-3-030-68446-4_10

Amadini, Roberto ; Gange, Graeme ; Schachte, Peter et al. / Algorithm selection for Dynamic Symbolic Execution : a preliminary study. Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings. editor / Maribel Fernández. Cham Switzerland : Springer, 2021. pp. 192-209 (Lecture Notes in Computer Science ).

@inproceedings{f1c9372b095545e0a836aa7cab695645,

title = "Algorithm selection for Dynamic Symbolic Execution: a preliminary study",

abstract = "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.",

keywords = "Algorithm selection, Constraint solving, Dynamic symbolic execution, Portfolio solving, Software verification",

author = "Roberto Amadini and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",

year = "2021",

doi = "10.1007/978-3-030-68446-4_10",

language = "English",

isbn = "9783030684457",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "192--209",

editor = "Maribel Fern{\'a}ndez",

booktitle = "Logic-Based Program Synthesis and Transformation",

note = "International Symposium on Logic-based Program Synthesis and Transformation 2020, LOPSTR 2020 ; Conference date: 07-09-2020 Through 09-09-2020",

url = "https://link.springer.com/book/10.1007/978-3-030-68446-4, https://nms.kcl.ac.uk/maribel.fernandez/LOPSTR2020/",

}

Amadini, R, Gange, G, Schachte, P, Søndergaard, H & Stuckey, PJ 2021, Algorithm selection for Dynamic Symbolic Execution: a preliminary study. in M Fernández (ed.), Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings. Lecture Notes in Computer Science , vol. 12561, Springer, Cham Switzerland, pp. 192-209, International Symposium on Logic-based Program Synthesis and Transformation 2020, Bologna, Italy, 7/09/20. https://doi.org/10.1007/978-3-030-68446-4_10

Algorithm selection for Dynamic Symbolic Execution: a preliminary study. / Amadini, Roberto; Gange, Graeme; Schachte, Peter et al.
Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings. ed. / Maribel Fernández. Cham Switzerland: Springer, 2021. p. 192-209 (Lecture Notes in Computer Science ; Vol. 12561).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Algorithm selection for Dynamic Symbolic Execution

T2 - International Symposium on Logic-based Program Synthesis and Transformation 2020

AU - Amadini, Roberto

AU - Gange, Graeme

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

N1 - Conference code: 30th

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

KW - Algorithm selection

KW - Constraint solving

KW - Dynamic symbolic execution

KW - Portfolio solving

KW - Software verification

UR - http://www.scopus.com/inward/record.url?scp=85102654403&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-68446-4_10

DO - 10.1007/978-3-030-68446-4_10

M3 - Conference Paper

AN - SCOPUS:85102654403

SN - 9783030684457

T3 - Lecture Notes in Computer Science

SP - 192

EP - 209

BT - Logic-Based Program Synthesis and Transformation

A2 - Fernández, Maribel

PB - Springer

CY - Cham Switzerland

Y2 - 7 September 2020 through 9 September 2020

ER -

Amadini R, Gange G, Schachte P, Søndergaard H, Stuckey PJ. Algorithm selection for Dynamic Symbolic Execution: a preliminary study. In Fernández M, editor, Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020 Bologna, Italy, September 7–9, 2020 Proceedings. Cham Switzerland: Springer. 2021. p. 192-209. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-030-68446-4_10

Algorithm selection for Dynamic Symbolic Execution: a preliminary study

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this