BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Fast and Reliable Formal Verification of Smart Contracts with the 
 Move Prover
DTSTART:20230803T150000
DTEND:20230803T160000
DTSTAMP:20260506T205832Z
UID:bb7cbda6491d863976d7f623de10a03d09c403fda90c90a2e2005b3e
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Meng Xu\, Cheriton School of Computer Science\, Universi
 ty of Waterloo\, Canada\nAbstract\nThe Move Prover (MVP) is a formal verif
 ier for smart contracts written in the Move programming language. MVP has 
 an expressive specification language\, and is fast and reliable enough tha
 t it can be run routinely by developers and in integration testing. Beside
 s the simplicity of smart contracts and the Move language\, three implemen
 tation approaches are responsible for the practicality of MVP: (1) an alia
 s-free memory model\, (2) fine-grained invariant checking\, and (3) monomo
 rphization.\nThe entirety of the Move code for the Diem blockchain has bee
 n extensively specified and can be completely verified by MVP in a few min
 utes. Changes in the Diem framework must be successfully verified before b
 eing integrated into the open-source repository on GitHub.\n\nBiography\n\
 nProf. Meng Xu is an Assistant Professor in the Cheriton School of Compute
 r Science at the University of Waterloo\, Canada. His research is in the a
 rea of system and software security\, with a focus on delivering high-qual
 ity solutions to practical security programs\, especially in finding and p
 atching vulnerabilities in critical computer systems. This usually include
 s research and development of automated program analysis / testing / verif
 ication tools that facilitate the security reasoning of critical programs
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR