Rust & Prusti: From a Safety-Focused Design To Formal Verification
Event start time 19.11.2020 16:15
Event end time 19.11.2020 18:15
Did you hear that Rust looks very promising but wonder whether it's just hype? Are you interested in understanding why Rust is frequently mentioned as one of the most beloved programming languages? Do you want to know which features are truly unique to Rust?
In this talk, we discuss what makes Rust a modern systems programming language. Apart from its key features and guarantees, we consider frequently misunderstood concepts, such as unsafe code, and how they are supposed to be applied. Moreover, we demonstrate that the Rust compiler's powerful type system and safety guarantees can be further exploited to enable lightweight formal verification of functional correctness properties.
Agenda
- Introduction: What Rust can(not) do for you
- Rust in a Nutshell
- A dive into Rust's distinguishing features: ownership, borrowing, lifetimes, and traits
- How (should) programmers use Unsafe Rust?
- Prusti: Leveraging the Rust compiler for formal verification
Administrative Details
The talk will be held over Zoom and the link will be sent shortly before the talk.
The fine print
By participating you agree that pictures can be taken of you that could be used for VIS-Purposes (VISIONEN, Instagram, etc)
By participating, you agree to adhere by the VIS Code of Conduct
Every participant is responsible for their own insurance
All statements are made without guarantee
In general, there are no refunds
Event organisers
Main event organiser Simon Meinhard