If you are attending ICSE (the IEEE/ACM International Conference on Software Engineering) in Ottawa this May, make sure to join us for "Symposium on Formal Methods for RUST" by Atlas Computing! Daniel and our team will be there!
Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) https://lu.ma/umi3g2wc Speaker highlight: Daniel Cumming has been a verification engineer for Runtime Verification Inc. for over 2 years, nearly exclusively working with #Rust code. Daniel has audited smart contracts for multiple Rust based blockchains, as well as infrastructure for the Stellar blockchain. He has also contributed to the #KMIR project which encodes the operational semantics of Rust's MIR via Stable MIR JSON through the K Framework. Daniel has also taught an introductory Rust boot camp at RareSkills since the start of 2025. Previous to working for RV, Daniel worked as a research assistant at The University of Queensland on projects related to ARM64 binary verification, and published a conference paper on EVM Bytecode verification using F* and Vale. The Talk: In this talk, I will present our roadmap and achievements in developing an integrated solution for symbolic execution of Rust code compiled to an externalized Stable MIR. At Runtime Verification Inc., we are developing Koat, a tool for the analysis and formal verification of Rust code (in general, whether unsafe or safe). It uses symbolic execution at the MIR level to analyze and verify Rust programs, by way of a precise semantics of Stable MIR defined in K Framework. This allows for describing program properties in the style of property tests, an established technique supported in many programming languages for randomized testing and fuzzing. Event registration page: https://lu.ma/umi3g2wc