Andrea Lattuada gives a talk at the Rust Dublin meetup

Andrea Lattuada gave the followinf talk at the Rust Dublin meetup:

Verus — Verified Rust for low-level systems code

Abstract: 

The Rust programming language, with its combination of high-level features, memory safety, and low-level "unsafe" primitives has proven to be an excellent tool to write high-performance systems software. Rust's properties and type system also make it an excellent basis for "full functional verification" where formal reasoning is used to prove that the behavior 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).

 

 

JavaScript has been disabled in your browser