Home > Research > Publications & Outputs > Quick verification of concurrent programs by it...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Quick verification of concurrent programs by iteratively relaxed scheduling

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Quick verification of concurrent programs by iteratively relaxed scheduling. / Metzler, P.; Saissi, H.; Bokor, P. et al.
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2017. p. 776-781.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Metzler, P, Saissi, H, Bokor, P, Suri, N, T.N., N (ed.), G., R (ed.) & M., DP (ed.) 2017, Quick verification of concurrent programs by iteratively relaxed scheduling. in 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, pp. 776-781. https://doi.org/10.1109/ASE.2017.8115688

APA

Metzler, P., Saissi, H., Bokor, P., Suri, N., T.N., N. (Ed.), G., R. (Ed.), & M., D. P. (Ed.) (2017). Quick verification of concurrent programs by iteratively relaxed scheduling. In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 776-781). IEEE. https://doi.org/10.1109/ASE.2017.8115688

Vancouver

Metzler P, Saissi H, Bokor P, Suri N, T.N. N, (ed.), G. R, (ed.) et al. Quick verification of concurrent programs by iteratively relaxed scheduling. In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE. 2017. p. 776-781 doi: 10.1109/ASE.2017.8115688

Author

Metzler, P. ; Saissi, H. ; Bokor, P. et al. / Quick verification of concurrent programs by iteratively relaxed scheduling. 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2017. pp. 776-781

Bibtex

@inproceedings{e69b4fe037584ba399b0cfd5442aed14,
title = "Quick verification of concurrent programs by iteratively relaxed scheduling",
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. {\textcopyright} 2017 IEEE.",
keywords = "Automation, Iterative methods, Scheduling, Software engineering, Software testing, Automated verification, Benchmark programs, Concurrent program, Concurrent software, Deterministic scheduling, Prototype implementations, Software verification, Verification complexity, Verification",
author = "P. Metzler and H. Saissi and P. Bokor and Neeraj Suri and Nguyen T.N. and Rosu G. and M., {Di Penta}",
year = "2017",
month = oct,
day = "30",
doi = "10.1109/ASE.2017.8115688",
language = "English",
isbn = "9781538639764",
pages = "776--781",
booktitle = "2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)",
publisher = "IEEE",

}

RIS

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 -