Modular formal verification of expressive low-level object-oriented programming languages

In this PhD project, we perform research on the theory and tool-building aspects of performing modular formal verification of safety and security properties of programs written in industrially-relevant programming languages such as C++, with the goal of making modular formal verification technology more applicable to industrial practice. Challenges include supporting C++ templates and the C++ Standard Template Library, and adding full support for treating structs or classes as values, which is not yet well-supported by existing technologies.