IRILL - Research and Innovation on Free Software
IRILL, Paris

L'Irill accueille la prochaine séance du séminaire de l'équipe APR (Algorithme, Programmation et Résolution) - LIP6 :

Séance du jeudi 20 octobre, 14h-16h :

Guillaume Bau (APR - LIP6 - SU // Nomadics Labs),

« Interprétation abstraite de smart-contracts Michelson avec MOPSA »

Résumé :

Michelson est le langage de smart-contracts de la blockchain Tezos. Dans cette présentation, nous allons aborder le développement d'un outil d'analyse statique pour ce langage reposant sur le framework d'interprétation abstraite MOPSA. Michelson est un langage à pile purement fonctionnel, fortement typé, disposant de structures de données de haut niveau comme les sets, maps et lambdas. Il a été conçu avec le souci de rendre explicite les erreurs à l'exécution comme les divisions par 0 ou les overflows. Nous présenterons les domaines abstraits utilisés dans cet analyseur permettant le support d'un langage à pile, ainsi queles structures de données de Michelson. Nous aborderons les analyses permettant de détecter erreurs à l'exécution (même si celles-ci sont rares), le développement du support de contexte d'exécution de la blockchain permettant le support d'analyses multi-appels (très différent du modèle conventionnel d'appel à une fonction dans un langage classique). Enfin, nous aborderons le développement d'analyses plus haut-niveau permettant la vérification de propriétés fonctionnel les d'un smart-contract d'échange distribué.

Lieu :

En chair et en os en salle 15-16/101 de l'IRILL (rotonde 15, 1er étage) 4 place Jussieu, 75005 Paris métro Jussieu (lignes 7 et 10)