Standard
Efficient verification of program fragments: Eager POR. / Metzler, P.; Saissi, H.; Bokor, P. et al.
Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Vol. 9938 LNCS Springer-Verlag, 2016. p. 375-391.
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Metzler, P, Saissi, H, Bokor, P, Hess, R
, Suri, N, Artho, C (ed.), Peled, D (ed.) & Legay, A (ed.) 2016,
Efficient verification of program fragments: Eager POR. in
Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. vol. 9938 LNCS, Springer-Verlag, pp. 375-391.
https://doi.org/10.1007/978-3-319-46520-3_24APA
Metzler, P., Saissi, H., Bokor, P., Hess, R.
, Suri, N., Artho, C. (Ed.), Peled, D. (Ed.), & Legay, A. (Ed.) (2016).
Efficient verification of program fragments: Eager POR. In
Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings (Vol. 9938 LNCS, pp. 375-391). Springer-Verlag.
https://doi.org/10.1007/978-3-319-46520-3_24Vancouver
Metzler P, Saissi H, Bokor P, Hess R
, Suri N, Artho C, (ed.) et al.
Efficient verification of program fragments: Eager POR. In Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Vol. 9938 LNCS. Springer-Verlag. 2016. p. 375-391 doi: 10.1007/978-3-319-46520-3_24
Author
Metzler, P. ; Saissi, H. ; Bokor, P. et al. /
Efficient verification of program fragments : Eager POR. Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Vol. 9938 LNCS Springer-Verlag, 2016. pp. 375-391
Bibtex
@inproceedings{1b3fff8d627342708dab048117e65be1,
title = "Efficient verification of program fragments: Eager POR",
abstract = "Software verification of concurrent programs is hampered by an exponentially growing state space due to non-deterministic process scheduling. Partial order reduction (POR)-based verification has proven to be a powerful technique to handle large state spaces. In this paper, we propose a novel dynamic POR algorithm, called Eager POR (epor), that requires considerably less overhead during state space exploration than existing algorithms. epor is based on a formal characterization of program fragments for which exploration can be scheduled in advance and dependency checks can be avoided. We show the correctness of this characterization and evaluate the performance of epor in comparison to existing state-of-the-art dynamic POR algorithms. Our evaluation shows substantial improvement in the runtime performance by up to 91%. {\textcopyright} Springer International Publishing AG 2016.",
keywords = "Concurrent programs, Model checking, Partial order reduction, Space research, State space methods, Concurrent program, Non-deterministic process, Partial order reductions, Program fragments, Run-time performance, Software verification, State of the art, State space exploration, Verification",
author = "P. Metzler and H. Saissi and P. Bokor and R. Hess and Neeraj Suri and C. Artho and D. Peled and A. Legay",
year = "2016",
month = sep,
day = "22",
doi = "10.1007/978-3-319-46520-3_24",
language = "English",
isbn = "9783319465197",
volume = "9938 LNCS",
pages = "375--391",
booktitle = "Automated Technology for Verification and Analysis",
publisher = "Springer-Verlag",
}
RIS
TY - GEN
T1 - Efficient verification of program fragments
T2 - Eager POR
AU - Metzler, P.
AU - Saissi, H.
AU - Bokor, P.
AU - Hess, R.
AU - Suri, Neeraj
A2 - Artho, C.
A2 - Peled, D.
A2 - Legay, A.
PY - 2016/9/22
Y1 - 2016/9/22
N2 - Software verification of concurrent programs is hampered by an exponentially growing state space due to non-deterministic process scheduling. Partial order reduction (POR)-based verification has proven to be a powerful technique to handle large state spaces. In this paper, we propose a novel dynamic POR algorithm, called Eager POR (epor), that requires considerably less overhead during state space exploration than existing algorithms. epor is based on a formal characterization of program fragments for which exploration can be scheduled in advance and dependency checks can be avoided. We show the correctness of this characterization and evaluate the performance of epor in comparison to existing state-of-the-art dynamic POR algorithms. Our evaluation shows substantial improvement in the runtime performance by up to 91%. © Springer International Publishing AG 2016.
AB - Software verification of concurrent programs is hampered by an exponentially growing state space due to non-deterministic process scheduling. Partial order reduction (POR)-based verification has proven to be a powerful technique to handle large state spaces. In this paper, we propose a novel dynamic POR algorithm, called Eager POR (epor), that requires considerably less overhead during state space exploration than existing algorithms. epor is based on a formal characterization of program fragments for which exploration can be scheduled in advance and dependency checks can be avoided. We show the correctness of this characterization and evaluate the performance of epor in comparison to existing state-of-the-art dynamic POR algorithms. Our evaluation shows substantial improvement in the runtime performance by up to 91%. © Springer International Publishing AG 2016.
KW - Concurrent programs
KW - Model checking
KW - Partial order reduction
KW - Space research
KW - State space methods
KW - Concurrent program
KW - Non-deterministic process
KW - Partial order reductions
KW - Program fragments
KW - Run-time performance
KW - Software verification
KW - State of the art
KW - State space exploration
KW - Verification
U2 - 10.1007/978-3-319-46520-3_24
DO - 10.1007/978-3-319-46520-3_24
M3 - Conference contribution/Paper
SN - 9783319465197
VL - 9938 LNCS
SP - 375
EP - 391
BT - Automated Technology for Verification and Analysis
PB - Springer-Verlag
ER -
