Lean Software Verification
Julian Sutherland ( Nethermind.io )
- 13:00 3rd May 2022 ( Trinity Term 2022 )LTA - Wolfson building Oxford
In this talk, we aim to demonstrate the use of proof assistants in software verification. To this end, will give a practical introduction to dependent types and their use in producing computer checkable proofs. We will then specify the semantics of a simple imperative programming language into the Lean proof assistant (https://leanprover.github.io/) and use it to prove some properties of a simple program.
This talk will be in-person in LTA wolfson building. We will also live stream via Teams using the folowing link
Microsoft Teams meeting
Join on your computer or mobile app
Speaker bio
Julian completed his PhD at Imperial College London in abstract termination verification for concurrency. Having previously worked in Facebook's static analysis team (Infer), he is now tech lead of Nethermind's formal verification team. This team aims to verify the Ethereum ecosystem using the Lean proof assistant and by developing formal verification tools.Share this:
