Name
Abstract | ||
|---|---|---|
The most prominent advantage of software verification over testing is a rigorous check of every possible software behavior. However, large state spaces of concurrent systems, due to non-deterministic scheduling, result in a slow automated verification process. Therefore, verification introduces a large delay between completion and deployment of concurrent software.
This paper introduces a novel iterative approach to verification of concurrent programs that drastically reduces this delay. By restricting the execution of concurrent programs to a small set of admissible schedules, verification complexity and time is drastically reduced. Iteratively adding admissible schedules after their verification eventually restores non-deterministic scheduling. Thereby, our framework allows to find a sweet spot between a low verification delay and sufficient execution time performance. Our evaluation of a prototype implementation on well-known benchmark programs shows that after verifying only few schedules of the program, execution time overhead is competitive to existing deterministic multi-threading frameworks.
|
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ASE.2017.8115688 | ASE |
Keywords | Field | DocType |
quick verification,iteratively relaxed scheduling,software verification,rigorous check,concurrent systems,nondeterministic scheduling,slow automated verification process,concurrent software,iterative approach,admissible schedules,verification complexity,low verification delay,sufficient execution time performance,software behavior,concurrent program verification,execution time overhead,deterministic multithreading frameworks | Model checking,Software deployment,Scheduling (computing),Computer science,Theoretical computer science,Schedule,Software,Concurrent computing,Small set,Distributed computing,Software verification | Conference |
ISSN | ISBN | Citations |
1527-1366 | 978-1-5386-2684-9 | 0 |
PageRank | References | Authors |
0.34 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Patrick Metzler | 1 | 0 | 1.69 |
| Habib Saissi | 2 | 8 | 4.23 |
| Péter Bokor | 3 | 29 | 5.14 |
| Neeraj Suri | 4 | 10 | 4.94 |