IWACO 2025
who it's for
verification tool developers, formal methods engineers, programming language researchers, Rust developers, systems programmers, memory safety engineers, research software engineers
topics
ownership types for Rust; move and copy semantics; multiple-owner stack frames; Verus-verified thread-safe array; permission-based interior mutability; unfold/fold semantics for verification; gradual verification with runtime checks; implicit dynamic frames for ownership; temporal resource typing with resettable timers; type universes as Kripke worlds
| title | author | length |
|---|---|---|
| Against Borrowing: Own the forest, not the trees! | James Noble | 40m |
Argues that Rust’s borrow checker is best understood as an ownership types system layered over classic OO ownership, not a novel separate mechanism… | ||
| A Verified Thread-Safe Array in Rust | Sasha Pak, Fabian Muehlboeck, Alex Potanin | 23m |
A verified thread-safe array API in Rust uses the Verus verifier and permission-based interior mutability to let shared references enable arbitrary parallel… | ||
| Unfolding Expressions for Gradual Verification | Hazel Torek, Long Tien Nguyen, Jonathan Aldrich | 26m |
Formalizes evaluation and proof obligations for unfolding expressions in gradual verification, giving both static (isorecursive) and dynamic (equirecursive)… | ||
| Gradual Verification: Assuring Software Incrementally | Jonathan Aldrich | 28m |
Proposes gradual verification that lets each assertion be complete, partial, or omitted and gives a sound mix of static and runtime checks so every spec… | ||
| Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning | Yiyuan Cao, Taro Sekiyama | 24m |
Type system enriches substructural resource types with a resettable timer that bounds progress through transition-system states and forces resources to reach… | ||
| Type Universes as Kripke Worlds: Memory Management Edition | Paulette Koronkevich | 22m |
Claims a tight correspondence between dependent-type type universe hierarchy and Kripke-style heap worlds, using a kinding discipline to forbid cross-level and… | ||
| nothing matches | ||