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