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 1st - 6th March 2023)
- Rust Nation 23 (in London on 16th - 17th February 2023)
- Rust Nation Pre-Conference Reception with The Rust Foundation (in London on 15th February 2023)
- Sharing is Caring? Comparing Ownership in Haskell and Rust (SkillsCast recorded in December 2022)
- Sharing is Caring? Comparing ownership in Haskell and Rust (SkillsCast recorded in December 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.