Name: Verus — Verified Rust for low-level systems code
Start: 2022-06-09T18:30:00+01:00
End: 2022-06-09T19:30:00+01:00

We're very pleased to be able to host a talk from Andrea Lattuada for our next talk.

In Andrea's words...

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).

Anton Whalley

Brian JG

Alan Ryan

Rust Dublin

Technology

Game Programming

Open Source

Web Development

Rust

Software Development

Programming Languages

Computer Programming

Verus — Verified Rust for low-level systems code

Online event

Share

Rust Dublin

Verus — Verified Rust for low-level systems code

Rust Dublin

Details

Members are also interested in