Parallel Symbolic Execution: Merging In-Flight Requests
Research output: Contribution to book/Conference proceedings/Anthology/Report › Chapter in book/Anthology/Report › Contributed › peer-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 language | English |
---|---|
Title of host publication | Hardware and Software: Verification and Testing |
Editors | Nir Piterman |
Publisher | Springer International Publishing |
Pages | 120-135 |
Number of pages | 16 |
Volume | 9434 |
ISBN (print) | 978-3-319-26286-4 |
Publication status | Published - 2015 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 9434 |
---|---|
ISSN | 0302-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