Our FP Syd meeting in August is on Monday 24 August at our sponsor Microsoft in North Sydney. We plan to have one full length talk:
Jost Berthold: *Verifying Rust Code with K Framework* (abstract below)
Short lightning talks of 5-10 minutes are also welcome.
As usual, the event will start around 6pm for snacks, drinks and networking. Talks will start around 6:45.
Please RSVP by the Friday before (noon) to be on the guest list, and arrive on time to ensure you get the lift to level 27.
We are always on the lookout for talk contributions. Our topic range is broad, covering a spectrum of functional and functionally-oriented programming, program verification, and more generally programming languages and their semantics and pragmatics. Please contact one of the organisers if you would like to contribute to our community.
----------------------------
Jost Berthold: *Verifying Rust Code with K Framework*
Rust is increasingly popular with system programmers as a safer alternative to C with a high degree of memory safety without sacrificing runtime performance. Rust programs aren't "safe by construction", though, a memory-safe program may still do the wrong thing. Consequently, Rust is an exciting target for verification.
This talk presents KMIR, an executable formal semantics of Rust's Stable (Public) MIR (Middle Intermediate Representation), written in the K Framework. The K Framework semantics toolbox, and a hook in the Rust compiler to extract its MIR during compilation, provide a way to interpret Rust programs, concretely or symbolically. This symbolic execution of a Rust program allows for verifying program properties and detection of undefined behaviour when run with arbitrary inputs.
We will provide an overview of the KMIR setup and the essentials of K Framework before discussing how MIR is encoded in K and its capabilities to date. The talk includes practical demonstrations of running and proving properties of small Rust programs.
