Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn about a practical model-checking methodology for verifying concurrency in Rust operating system kernels through this 15-minute conference presentation from USENIX ATC '25. Discover how researchers developed CONVEROS, a formal verification approach specifically designed to check the correctness of concurrency modules in ASTERINAS, an open-source Linux-compatible operating system written in Rust. Explore the multi-layered, multi-grained specification methodology that makes formal verification more accessible and cost-effective by using PlusCal specifications for Rust code, enabling incremental and automated conformance checking to detect specification-code discrepancies. Examine the practical application of CONVEROS to 12 critical concurrency modules including synchronization primitives and thread-safety components, which successfully uncovered 20 bugs leading to data races, deadlocks, livelocks, and kernel panics. Understand how this approach achieves a specification-to-code ratio of 0.3 to 2.3 with only four person-months of verification effort, demonstrating that formal methods can be made practical and adaptable for evolving operating system code while maintaining the rigor necessary for critical system verification.
