Model Checking C++ with Exceptions

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00077485" target="_blank" >RIV/00216224:14330/14:00077485 - isvavai.cz</a>

Result on the web

<a href="http://journal.ub.tu-berlin.de/eceasst/article/view/983" target="_blank" >http://journal.ub.tu-berlin.de/eceasst/article/view/983</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Model Checking C++ with Exceptions

Original language 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 extensionscan be used to elegantly implement other features with non-local control transfer, most importantly the longjmp function in C.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

—

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2014

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Electronic Communications of the EASST

ISSN

1863-2122

e-ISSN

—

Volume of the periodical

70

Issue of the periodical within the volume

Listopad

Country of publishing house

DE - GERMANY

Number of pages

15

Pages from-to

1-15

UT code for WoS article

—

EID of the result in the Scopus database

—