Back to Blog Tracking Rust's aliasing model can be quadratically expensive if done naively. Learn how we fixed this in Soteria Rust by doing meta garbage collection. Soteria Rust is a symbolic execution tool for verifying Rust programs; it explores every execution path, catching undefined behaviour, aliasing errors, and more. We recently noticed something odd: a simple loop that increments a variable N times was taking quadratic time in N! The culprit was our implementation of Tree Borrows , ...