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

PETS - July 16, 2021

HashWires: Hyperefficient Credential-Based Range Proofs

Konstantinos (Kostas) Chalkias, Shir Cohen, Kevin Lewi, Fredric Moezinia, Yolan Romailler

ICML - July 17, 2021

Recovering AES Keys with a Deep Cold Boot Attack

Itamar Zimerman, Eliya Nachmani, Lior Wolf

Trusted Smart Contracts Workshop at Financial Cryptography (FC) - May 12, 2021

Reactive Key-Loss Protection in Blockchains

Sam Blackshear, Konstantinos (Kostas) Chalkias, Panagiotis Chatzigiannis, Riyaz Faizullabhoy, Irakliy Khaburzaniya, Lefteris Kokoris Kogias, Joshua Lind, David Wong, Tim Zakian

VLDB - July 31, 2021

CALYPSO: Private Data Management for Decentralized Ledgers

Eleftherios Kokoris-Kogias, Enis Ceyhun Alp, Linus Gasser, Philipp Jovanovic, Ewa Syta, Bryan Ford

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: Cookie Policy