Parallel Symbolic Execution: Merging In-Flight Requests
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Buch/Sammelband/Gutachten › Beigetragen › Begutachtung
Beitragende
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
Originalsprache | Englisch |
---|---|
Titel | Hardware and Software: Verification and Testing |
Redakteure/-innen | Nir Piterman |
Herausgeber (Verlag) | Springer International Publishing |
Seiten | 120-135 |
Seitenumfang | 16 |
Band | 9434 |
ISBN (Print) | 978-3-319-26286-4 |
Publikationsstatus | Veröffentlicht - 2015 |
Peer-Review-Status | Ja |
Publikationsreihe
Reihe | Lecture Notes in Computer Science, Volume 9434 |
---|---|
ISSN | 0302-9743 |
Externe IDs
Scopus | 84950295857 |
---|
Schlagworte
Forschungsprofillinien der TU Dresden
DFG-Fachsystematik nach Fachkollegium
Schlagwörter
- Symbolic Execution, Path Constraint, Ring Buffer, State Space Explosion, Workk Thread