Ivan Beschastnikh

Modular Responsiveness Verification of Rust Async Runtimes

This work presents a lightweight and modular proof technique for verifying eventual progression guarantees for Rust async runtimes and realizes this proof technique as a set of static analyses for Rust and uses these to verify eventual progression of several key components of multiple Rust async runtime implementations...