Rust promises to be a (memory) safe language. However, it doesn't mean that runtime errors are absent from Rust codebases. Execution faults can still happen, both in mixed code bases that tap into the vast library of existing C and C++ codes and in code entirely wrote in Rust, even in "safe" mode.
In this presentation, we will discuss how these errors can occur in mixed code bases, with special attention to the type of runtime errors that can happen in C, C++ and Rust. We will explain how formal methods work, how they can exhaustively detect runtime errors, and how they can be refined to keep false positives to a minimum. We will also compare the pros and the cons of using formal methods to analyze mixed code bases within a single analysis rather than analyzing languages separately.