Aarhus University Seal / Aarhus Universitets segl

Talk by visiting researcher Thomas Sibut-Pinote on Mechanizing the Semantics of Tezos’ Bytecode in F*

26.08.2019 | Malene B.B. Andersen

Date Thu 29 Aug
Time 14:30 15:30
Location Nygaard-295 (building 5335, room 295), Dept. of Computer Science, Åbogade 34, 8200 Aarhus N

Title: Mechanizing the Semantics of Tezos’ Bytecode in F*

Abstract:  In this presentation from 2017, I will recall work done during an internship towards the mechanization of the semantics of Michelson, the opcode language of the Tezos cryptocurrency, using the F* theorem prover. Partial correctness of simple contracts was achieved. We managed to cross-compile of our Fstar code with the rest of the Tezos Ocaml codebase and confront it to their standard benchmarks.

About the speaker: Thomas Sibut-Pinote is a PhD student at Inria Saclay/École Polytechnique https://specfun.inria.fr/~tsibutpi/

About the talk: The talk is open to everyone interested and is organized by the Concordium Blockchain Research Center Aarhus. For further information about the research center, please visit the center website: http://cs.au.dk/research/centers/concordium/

COBRA, CS frontpage, Featured, Public/media