Verus - Verified Rust for low-level systems code by Andrea Lattuada - Rust Zürisee June 2023
Rust programmers care about the correctness of their code and, while the Rust type system and its memory safety are excellent foundations, they aren’t sufficient to ensure correctness. “Full functional verification" of code is an alternative (or a complement) to tests that uses formal methods to prove that the behaviour of a complex program corresponds to a desired specification, i.e. to prove that the program is "correct".
We are building our new tool, Verus, to efficiently verify full functional correctness of low-level systems code written in a safe Rust dialect that supports expressing specifications and proofs. In this talk I'll introduce the basics of functional verification, the verification technique used by Verus, and I'll demonstrate how the tool, with the programmer's help, can ensure that programs are bug-free (or how it catches bugs, if they are any).
Slides: https://github.com/rust-zurichsee/mee...
Guillaume's Blog: https://andrea.lattuada.me/
Would you like to chat or give a talk? Join us in our Matrix room:
https://matrix.to/#/#rust-zuerisee:matrix.coredump.ch
Support the Zürich community: https://estada.ch/support-my-work/
Chapters:
00:00 Introduction
01:19 Examples
38:40 Questions
Watch video Verus - Verified Rust for low-level systems code by Andrea Lattuada - Rust Zürisee June 2023 online without registration, duration hours minute second in high quality. This video was added by user Rust 26 June 2023, don't forget to share it with your friends and acquaintances, it has been viewed on our site 4,19 once and liked it 10 people.