| ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, vol. 128, 15 October 2016, p. 68-85. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2016.05.007. |
Other formats:
BibTeX
LaTeX
RIS
@article{1352228,
author = {Ročkai, Petr and Barnat, Jiří and Brim, Luboš},
article_number = {15 October 2016},
doi = {http://dx.doi.org/10.1016/j.scico.2016.05.007},
keywords = {Model checking; C++; Exception handling; LLVM},
language = {eng},
issn = {0167-6423},
journal = {Science of Computer Programming},
title = {Model checking C++ programs with exceptions},
url = {http://dx.doi.org/10.1016/j.scico.2016.05.007},
volume = {128},
year = {2016}
}
TY - JOUR
ID - 1352228
AU - Ročkai, Petr - Barnat, Jiří - Brim, Luboš
PY - 2016
TI - Model checking C++ programs with exceptions
JF - Science of Computer Programming
VL - 128
IS - 15 October 2016
SP - 68-85
EP - 68-85
PB - Elsevier B.V.
SN - 01676423
KW - Model checking
KW - C++
KW - Exception handling
KW - LLVM
UR - http://dx.doi.org/10.1016/j.scico.2016.05.007
N2 - We present an extension of the DIVINE software model checker to support programs with exception handling. The extension consists of two parts, a language-neutral implementation of the LLVM exception-handling instructions, and an adaptation of the C++ runtime for the DIVINE/LLVM exception model. This constitutes an important step towards support of both the full C++ specification and towards verification of real-world C++ programs using a software model checker. Additionally, we show how these extensions can be used to elegantly implement other features with non-local control transfer, most importantly the longjmp function in C.
ER -
ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Model checking C++ programs with exceptions. \textit{Science of Computer Programming}. Elsevier B.V., 2016, vol.~128, 15 October 2016, p.~68-85. ISSN~0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2016.05.007.
|
