Arrow Research search
Back to LOPSTR

LOPSTR 2020

Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study

Conference Paper Verification Formal Methods · Logic in Computer Science

Abstract

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.

Authors

Keywords

No keywords are indexed for this paper.

Context

Venue
International Symposium on Logic-Based Program Synthesis and Transformation
Archive span
1990-2025
Indexed papers
560
Paper id
376852642791219366