Evènement pour le groupe Séminaire Méthodes Formelles


Date 2020-10-06  14:00-15:00
TitreUsing TLA+ and Apalache to specify and check the Tendermint light client 
RésuméTLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. At Informal Systems, we are using TLA+ to specify and reason about the protocols that are implemented in the Tendermint blockchains and Cosmos ecosystem. In this talk, I give an introduction into Apalache, a symbolic model checker for TLA+. It assumes that all specification parameters are fixed and all states are finite structures. Apalache translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers, while keeping the verification problems decidable. Recently, we have designed the Tendermint light client protocol. The light client checks, whether a block originates from the blockchain, without retrieving and verifying all the blocks of the blockchain. I will present our solutions to modeling this protocol in TLA+ and model checking it with Apalache. Bio: Igor Konnov is a principal scientist at Informal Systems (Austria), a spin-off of Interchain Foundation (Switzerland). Igor is leading research and development of Apalache -- a symbolic model checker for TLA+. Before joining Informal Systems and Interchain Foundation, Igor Konnov worked as a researcher at Inria Nancy (France) and as a postdoc at TU Wien (Austria). He received his MSc and Ph.D. in Applied Mathematics and Computer Science from Lomonosov Moscow State University (Russia) in 2003 and 2009. In 2019, Igor received his Habilitation from TU Wien (Austria). 
LieuVirtual 
OrateurIgor Konnov 
Emailhttps://team.inria.fr/veridis/konnov/ 
UrlINRIA Nancy 



Aucun document lié à cet événement.

Retour
Retour à l'index