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 8th - 15th June 2022)
- Embedded Rust: Beginners Workshop (Online Workshop on 30th June 2022)
- LDN Talks May 2022 - Quickwit Takeover (in London on 30th May 2022)
- Rust in 2024 (SkillsCast recorded in May 2022)
- Rust's Unique Ownership Concept: Practical Examples and Why It's Important (SkillsCast recorded in May 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.