Parallel Symbolic Execution: Merging In-Flight Requests

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in Buch/Sammelband/GutachtenBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelHardware and Software: Verification and Testing
Redakteure/-innenNir Piterman
Herausgeber (Verlag)Springer International Publishing
Seiten120-135
Seitenumfang16
Band9434
ISBN (Print)978-3-319-26286-4
PublikationsstatusVeröffentlicht - 2015
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 9434
ISSN0302-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

Bibliotheksschlagworte