It's weird to see no mention in this post of separation logic, which would seem to provide a basic, general foundation for most of these techniques if perhaps not all of them. For instance, the RustBelt paper gives a description of Rust borrow checking that can arguably be understood as relying on some form of separation logic.