SkillsCast
Formal Verification of Subsets of the Rust Language
SkillsCast
Finally, I will shortly reflect on the status of formal verification in these subsets of rust.
About the Speaker
In this presentation, I will give a very brief introduction to interactive formal verification of programming languages.
I will then proceed with an overview of three projects that we are working on or contributing to in our CoBRA institute.
- ConCert, a framework for smart contract verification. As part of this we have developed a general backend to the Coq proof assistant which allows us to generate provably correct functional rust programs.
- hacspec, a subset of rust for the specification of high assurance cryptography.
- fiat-crypto, a verified compiler which allows one to generate efficient, provably correct, constant time and platform independent implementations of cryptographic primitives.
Finally, I will shortly reflect on the status of formal verification in these subsets of rust.
YOU MAY ALSO LIKE:
- Introduction to Rust (Online Workshop on 5th - 10th December 2022)
- Embedded Rust: Beginners Workshop (Online Workshop on 8th December 2022)
- Rust-Meetup (Online Meetup on 5th October 2022)
- Rust Nürnberg online #18 (Online Meetup on 6th October 2022)
- Bytecode Rewrite Optimizations (SkillsCast recorded in August 2022)
- Building Rust Projects with Nix and Bazel (SkillsCast recorded in June 2022)
Formal Verification of Subsets of the Rust Language
Bas Spitters
Associate professor Computer Science at Aarhus University. He leads the formal verification and smart contract parts of the CoBRA research center. His research focuses on type theory and formal verification, especially in the context of blockchains. This includes programming languages and high assurance cryptography.