| Identifikační kód | RIV/00216224:14330/14:00077485 |
|---|
| Název v anglickém jazyce | Model Checking C++ with Exceptions |
|---|
| Druh | J - Článek v odborném periodiku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Petr Ročkai (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 1292358)
Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) |
|---|
| Popis výsledku v anglickém jazyce | 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 extensionscan be used to elegantly implement other features with non-local control transfer, most importantly the longjmp function in C. |
|---|
| Klíčová slova oddělená středníkem | model checking; C++ exception handling; LLVM |
|---|
| Stránka www, na které se nachází výsledek | http://journal.ub.tu-berlin.de/eceasst/article/view/983 |
|---|