Model Checking C++ with Exceptions

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	ROČKAI Petr BARNAT Jiří BRIM Luboš
Year of publication	2014
Type	Article in Periodical
Magazine / Source	Electronic Communications of the EASST
MU Faculty or unit	Faculty of Informatics
Citation
Web	http://journal.ub.tu-berlin.de/eceasst/article/view/983
Doi	http://dx.doi.org/10.14279/tuj.eceasst.70.983
Field	Informatics
Keywords	model checking; C++ exception handling; LLVM
Description	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.
Related projects:	Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.