J 2016

Model checking C++ programs with exceptions

ROČKAI, Petr, Jiří BARNAT a Luboš BRIM

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

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í

Odkazy

Impakt faktor

Impact factor: 1.064

Kód RIV

RIV/00216224:14330/16:00088092

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000380595400005

Klíčová slova anglicky

Model checking; C++; Exception handling; LLVM

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 17. 4. 2018 08:35, prof. RNDr. Luboš Brim, CSc.

Anotace

V originále

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