Model checking C++ programs with exceptions

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	ROČKAI Petr BARNAT Jiří BRIM Luboš
Rok publikování	2016
Druh	Článek v odborném periodiku
Časopis / Zdroj	Science of Computer Programming
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1016/j.scico.2016.05.007
Doi	https://doi.org/10.1016/j.scico.2016.05.007
Obor	Informatika
Klíčová slova	Model checking; C++; Exception handling; LLVM
Popis	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.
Související projekty:	Correctness Analysis of C and C++ Programs with Threads