10-13, 13:30–14:00 (America/Bogota), Talk 4
In this talk, we present our work on formally specifying and verifying the Distributed Validator Technology (DVT) protocol, using the verification-ready programming language Dafny, to ensure that the DVT protocol behaves as expected. You will learn how to read the formal specification, how to use it to write your own implementation of the protocol, what properties we have formally proven to be guaranteed by the protocol and what the future directions of the DVT protocol and our work are.
Roberto is currently leading the Dependable Distributed Systems research team at ConsenSys. His main research interests revolve around the design, analysis and formal verification of distributed protocols.