Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust. - Arnaud Golfouse; Armaël Guéneau; Jacques-Henri Jourdan (CPP, 2026)