Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - Quick verification of concurrent programs by iteratively relaxed scheduling
AU - Metzler, P.
AU - Saissi, H.
AU - Bokor, P.
AU - Suri, Neeraj
A2 - T.N., Nguyen
A2 - G., Rosu
A2 - M., Di Penta
PY - 2017/10/30
Y1 - 2017/10/30
N2 - 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. © 2017 IEEE.
AB - 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. © 2017 IEEE.
KW - Automation
KW - Iterative methods
KW - Scheduling
KW - Software engineering
KW - Software testing
KW - Automated verification
KW - Benchmark programs
KW - Concurrent program
KW - Concurrent software
KW - Deterministic scheduling
KW - Prototype implementations
KW - Software verification
KW - Verification complexity
KW - Verification
U2 - 10.1109/ASE.2017.8115688
DO - 10.1109/ASE.2017.8115688
M3 - Conference contribution/Paper
SN - 9781538639764
SP - 776
EP - 781
BT - 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
PB - IEEE
ER -