Publication

The Move Prover

International Conference on Computer-Aided Verification (CAV)


Abstract

The Libra blockchain is designed to store billions of dollars in assets, so the security of code that executes transactions is important. The Libra blockchain has a new language for implementing transactions, called “Move.” This paper describes the Move Prover, an automatic formal verification system for Move. We overview the unique features of the Move language and then describe the architecture of the Prover, including the language for formal specification and the translation to the Boogie intermediate verification language.

Related Publications

All Publications

Distributed Auditing Proofs of Liabilities

Kostas Chalkias, Kevin Lewi, Payman Mohassel, Valeria Nikolaenko

ZKProof - April 22, 2020

Armada: Low-Effort Verification of High-Performance Concurrent Programs

Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao

PLDI - July 15, 2020

Winkle: Foiling Long-Range Attacks in Proof-of-Stake Systems

Sarah Azouvi, George Danezis, Valeria Nikolaenko

AFT - October 23, 2020

Inductive Sequentialization of Asynchronous Programs

Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer

PLDI - July 15, 2020

To help personalize content, tailor and measure ads, and provide a safer experience, we use cookies. By clicking or navigating the site, you agree to allow our collection of information on and off Facebook through cookies. Learn more, including about available controls: Cookies Policy