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

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2017
Type Article in Proceedings
Conference IEEE International Conference on Software Quality, Reliability and Security - QRS 2017
MU Faculty or unit

Faculty of Informatics

Citation
Web http://ieeexplore.ieee.org/document/8009908/
Doi http://dx.doi.org/10.1109/QRS.2017.15
Field Informatics
Keywords C++; Exceptions; Verification; Testing; Model Checking; DIVINE
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.