Symbolic Testing for Rust with crux-mir

Explore symbolic testing for Rust with crux-mir in this 42-minute conference talk presented by Aaron Tomb and Stuart Pernsteiner. Dive into the general features, targets, and design architecture of crux-mir, including its use of the Crucible language and symbolic execution strategy. Examine how crux-mir handles Rust's memory model, generics, iterator adapters, and monomorphization. Learn about the tool's approach to unsafe code, raw pointers, transmute and integer casts, low-level pointer offsets, and the slice library. Discover the Cargo integration and future work planned for crux-mir. The talk concludes with a Q&A session covering topics such as model organization, dynamic symbolic execution, multiple shared references, and handling of string and C intrinsics.