The Move Prover

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 syste...

Descripción completa

Detalles Bibliográficos
Autores principales: Zhong, Jingyi Emma, Cheang, Kevin, Qadeer, Shaz, Grieskamp, Wolfgang, Blackshear, Sam, Park, Junkil, Zohar, Yoni, Barrett, Clark, Dill, David L.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363214/
http://dx.doi.org/10.1007/978-3-030-53288-8_7
Descripción
Sumario: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 .

Ejemplares similares