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 and Jiří BARNAT

Basic information

Original name

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

Authors

ŠTILL, Vladimír (203 Czech Republic, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

IEEE

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/17:00095127

Organization unit

Faculty of Informatics

ISBN

978-1-5386-0592-9

DOI

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

UT WoS

000426842400006

Keywords in English

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

Abstract

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.

Links

GA15-08772S, research and development project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

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

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

ŠTILL, Vladimír, Petr ROČKAI and 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, p. 54-64. ISBN 978-1-5386-0592-9. Available from: 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 and 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, p.~54-64. ISBN~978-1-5386-0592-9. Available from: https://dx.doi.org/10.1109/QRS.2017.15.

Detailed Information on Publication Record