Parallel Symbolic Execution: Merging In-Flight Requests

Research output: Contribution to book/conference proceedings/anthology/reportChapter in book/anthology/reportContributedpeer-review



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.


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

Publication series

SeriesLecture Notes in Computer Science, Volume 9434

External IDs

Scopus 84950295857


Research priority areas of TU Dresden

DFG Classification of Subject Areas according to Review Boards


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

Library keywords