Model checking C++ programs with exceptions

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.

Základní údaje

• Originální název: Model checking C++ programs with exceptions
• Autoři: ROČKAI, Petr (703 Slovensko, domácí), Jiří BARNAT (203 Česká republika, garant, domácí) a Luboš BRIM (203 Česká republika, domácí).
• Vydání: Science of Computer Programming, Elsevier B.V. 2016, 0167-6423.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Článek v odborném periodiku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Nizozemské království
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Impakt faktor: Impact factor: 1.064
• Kód RIV: RIV/00216224:14330/16:00088092
• Organizační jednotka: Fakulta informatiky
• Doi: http://dx.doi.org/10.1016/j.scico.2016.05.007
• UT WoS: 000380595400005
• Klíčová slova anglicky: Model checking; C++; Exception handling; LLVM
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Návaznosti

• GA15-08772S, projekt VaV: Název: Analýza korektnosti vícevláknových programů v C a C++

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads