Towards Automatic Verification of Unsafe Rust with Constrained Horn Solvers

Explore an in-depth conference talk on the automatic verification of unsafe Rust code using constrained Horn solvers, presented by Zafer Esen, Philipp Rümmer, and Amanda Stjerna. Gain insights into cutting-edge techniques for ensuring the safety and reliability of Rust programs that utilize unsafe features, and learn how constrained Horn solvers can be leveraged to automate the verification process.

Towards Automatic Verification of Unsafe Rust with Constrained Horn Solvers