Latest COVID-19 Information for Purdue University

The Center for Education and Research in Information Assurance and Security (CERIAS)

The Center for Education and Research in
Information Assurance and Security (CERIAS)

Meng Xu - University of Waterloo

Students: Spring 2022, unless noted otherwise, sessions will be virtual on Zoom.

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

Nov 30, 2022


The Move Prover (MVP) is a formal verifier forsmart contracts written In the Move programming language. MVP has an expressivespecification language, and is fast and reliable enough that it can be runroutinely by developers and in integration testing. Besides the simplicity ofsmart contracts and the Move language, three implementation approaches areresponsible for the practicality of MVP: (1) an alias-free memory model, (2)fine-grained invariant checking, and (3) monomorphization. The entirety of theMove code for the Diem blockchain has been extensively specified and can becompletely verified by MVP in a few minutes. Changes in the Diem framework mustbe successfully verified before being integrated into the open sourcerepository on GitHub.

About the Speaker

Dr.Meng Xu is an Assistant Professor in the Cheriton School of Computer Science atthe University of Waterloo, Canada. His research is in the area of system andsoftware security, with a focus on delivering high-quality solutions topractical security programs, especially in finding and patching vulnerabilitiesin critical computer systems. This usually includes research and development ofautomated program analysis/ testing / verification tools that facilitate thesecurity reasoning of critical programs.

Ways to Watch


Watch Now!

Over 500 videos of our weekly seminar and symposia keynotes are available on our YouTube Channel. Also check out Spaf's YouTube Channel. Subscribe today!