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

## TL;DR

This paper presents a method to support C++ exceptions in formal verification by leveraging an intermediate language, DiVM, and off-the-shelf exception support components, simplifying verification of complex C++ programs.

## Contribution

It introduces a novel approach to incorporate C++ exception handling into verification workflows using DiVM and existing exception support components.

## Key findings

- Successfully integrated C++ exception support into DiVM-based verification.
- Reduced complexity by leveraging existing exception handling components.
- Enhanced verification capabilities for C++ programs with exceptions.

## Abstract

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.