ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, roč. 128, 15 October 2016, s. 68-85. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2016.05.007. |
Další formáty:
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 a Luboš BRIM. Model checking C++ programs with exceptions. \textit{Science of Computer Programming}. Elsevier B.V., 2016, roč.~128, 15 October 2016, s.~68-85. ISSN~0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2016.05.007.
|