Parallel Symbolic Execution: Merging In-Flight Requests

Research output: Contribution to book/Conference proceedings/Anthology/ReportChapter in book/Anthology/ReportContributedpeer-review

Contributors

Abstract

The strength of symbolic execution is the systematic analysis and validation of all possible control flow paths of a program and their respective properties, which is done by use of a solver component. Thus, it can be used for program testing in many different domains, e.g. test generation, fault discovery, information leakage detection, or energy consumption analysis. But major challenges remain, notably the huge (up to infinite) number of possible paths and the high computation costs generated by the solver to check the satisfiability of the constraints imposed by the paths. To tackle these challenges, researchers proposed the parallelization of symbolic execution by dividing the state space and handling the parts independently. Although this approach scales out well, we can further improve it by proposing a thread-based parallelized approach. It allows us to reuse shared resources like caches more efficiently – a vital part to reduce the solving costs. More importantly, this architecture enables us to use a new technique, which merges parallel incoming solver requests, leveraging incremental solving capabilities provided by modern solvers. Our results show a reduction of the solver time up to 50 % over the multi-threaded execution.

Details

Original languageEnglish
Title of host publicationHardware and Software: Verification and Testing
EditorsNir Piterman
PublisherSpringer International Publishing
Pages120-135
Number of pages16
Volume9434
ISBN (print)978-3-319-26286-4
Publication statusPublished - 2015
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 9434
ISSN0302-9743

External IDs

Scopus 84950295857

Keywords

Research priority areas of TU Dresden

DFG Classification of Subject Areas according to Review Boards

Keywords

  • Symbolic Execution, Path Constraint, Ring Buffer, State Space Explosion, Workk Thread

Library keywords