As C++ developers explore Rust for new development, the challenge of interoperability between the two languages grows. Large-scale C++ codebases now integrate Rust, requiring the use of the C ABI, which introduces risks like undefined behavior in C++ and runtime panics in Rust. Today, formal verification is often limited to specific programming languages (Ada, C, C++), with few tools supporting mixed-language environments. As Rust adoption increases alongside C++, new formal verification tools must evolve to ensure safe, predictable interactions between Rust and C++ libraries.
This talk explores how formal verification techniques can be adapted to hybrid systems to detect runtime errors both within the language-specific segments and across the language divide. We will also provide a few coded examples to illustrate how formal methods can be leveraged to pinpoint these errors with no false negatives and a low percentage of false positives.
View Slides
Steve Barriault is Vice President Technical Business Development at TrustInSoft, the leader in the use of formal methods for the detection of bugs in safety and security-critical applications. He has more than 20 years of experience in Embedded Software, working for the embedded division of Canonical (Ubuntu), Vector, and PolySpace, his teams and he providing complex solutions to a slew of prestigious clients in Automotive, Avionics, Medical Devices, Industrial Systems, Edge, and more.
Steve proudly wears his software engineering cap and loves to discuss how technologies can be leveraged for the benefit of all. He speaks English, French and Chinese fluently, studies Japanese at an intermediate/advanced level, and holds multiple degrees in Business, Sciences, Computer Science and International Relations.