Using Off-the-Shelf Exception Support Components in C++
Verification

D 2017

Using Off-the-Shelf Exception Support Components in C++ Verification

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT

Základní údaje

Originální název

Using Off-the-Shelf Exception Support Components in C++ Verification

Autoři

ŠTILL, Vladimír (203 Česká republika, domácí), Petr ROČKAI (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí)

Vydání

Neuveden, IEEE International Conference on Software Quality, Reliability and Security - QRS 2017, od s. 54-64, 11 s. 2017

Nakladatel

IEEE

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/17:00095127

Organizační jednotka

Fakulta informatiky

ISBN

978-1-5386-0592-9

DOI

http://dx.doi.org/10.1109/QRS.2017.15

UT WoS

000426842400006

Klíčová slova anglicky

C++; Exceptions; Verification; Testing; Model Checking; DIVINE

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 10. 2018 16:25, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

V originále

An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the 'libunwind' platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.

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

MUNI/A/0897/2016, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0992/2016, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. Online. In IEEE International Conference on Software Quality, Reliability and Security - QRS 2017. Neuveden: IEEE, 2017, s. 54-64. ISBN 978-1-5386-0592-9. Dostupné z: https://dx.doi.org/10.1109/QRS.2017.15.

@inproceedings{1394157,
   author = {Štill, Vladimír and Ročkai, Petr and Barnat, Jiří},
   address = {Neuveden},
   booktitle = {IEEE International Conference on Software Quality, Reliability and Security - QRS 2017},
   doi = {http://dx.doi.org/10.1109/QRS.2017.15},
   keywords = {C++; Exceptions; Verification; Testing; Model Checking; DIVINE},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-1-5386-0592-9},
   pages = {54-64},
   publisher = {IEEE},
   title = {Using Off-the-Shelf Exception Support Components in C++ Verification},
   url = {http://ieeexplore.ieee.org/document/8009908/},
   year = {2017}
}

TY  - JOUR
ID  - 1394157
AU  - Štill, Vladimír - Ročkai, Petr - Barnat, Jiří
PY  - 2017
TI  - Using Off-the-Shelf Exception Support Components in C++ Verification
PB  - IEEE
CY  - Neuveden
SN  - 9781538605929
KW  - C++
KW  - Exceptions
KW  - Verification
KW  - Testing
KW  - Model Checking
KW  - DIVINE
UR  - http://ieeexplore.ieee.org/document/8009908/
L2  - http://ieeexplore.ieee.org/document/8009908/
N2  - An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the 'libunwind' platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.
ER  -

ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. Online. In \textit{IEEE International Conference on Software Quality, Reliability and Security - QRS 2017}. Neuveden: IEEE, 2017, s.~54-64. ISBN~978-1-5386-0592-9. Dostupné z: https://dx.doi.org/10.1109/QRS.2017.15.

Podrobný výpis o publikaci