Další formáty:
BibTeX
LaTeX
RIS
@article{1210603,
author = {Ročkai, Petr and Barnat, Jiří and Brim, Luboš},
article_number = {Listopad},
doi = {http://dx.doi.org/10.14279/tuj.eceasst.70.983},
keywords = {model checking; C++ exception handling; LLVM},
language = {eng},
issn = {1863-2122},
journal = {Electronic Communications of the EASST},
title = {Model Checking C++ with Exceptions},
url = {http://journal.ub.tu-berlin.de/eceasst/article/view/983},
volume = {70},
year = {2014}
}
TY - JOUR
ID - 1210603
AU - Ročkai, Petr - Barnat, Jiří - Brim, Luboš
PY - 2014
TI - Model Checking C++ with Exceptions
JF - Electronic Communications of the EASST
VL - 70
IS - Listopad
SP - 1-15
EP - 1-15
SN - 18632122
KW - model checking
KW - C++ exception handling
KW - LLVM
UR - http://journal.ub.tu-berlin.de/eceasst/article/view/983
L2 - http://journal.ub.tu-berlin.de/eceasst/article/view/983
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 a Luboš BRIM. Model Checking C++ with Exceptions. \textit{Electronic Communications of the EASST}. 2014, roč.~70, Listopad, s.~1-15. ISSN~1863-2122. Dostupné z: https://dx.doi.org/10.14279/tuj.eceasst.70.983.
|
