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
_version_ 1783559624665858048
author Zhong, Jingyi Emma
Cheang, Kevin
Qadeer, Shaz
Grieskamp, Wolfgang
Blackshear, Sam
Park, Junkil
Zohar, Yoni
Barrett, Clark
Dill, David L.
author_facet Zhong, Jingyi Emma
Cheang, Kevin
Qadeer, Shaz
Grieskamp, Wolfgang
Blackshear, Sam
Park, Junkil
Zohar, Yoni
Barrett, Clark
Dill, David L.
author_sort Zhong, Jingyi Emma
collection PubMed
description 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 .
format Online
Article
Text
id pubmed-7363214
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73632142020-07-16 The Move Prover Zhong, Jingyi Emma Cheang, Kevin Qadeer, Shaz Grieskamp, Wolfgang Blackshear, Sam Park, Junkil Zohar, Yoni Barrett, Clark Dill, David L. Computer Aided Verification Article 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 . 2020-06-13 /pmc/articles/PMC7363214/ http://dx.doi.org/10.1007/978-3-030-53288-8_7 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Zhong, Jingyi Emma
Cheang, Kevin
Qadeer, Shaz
Grieskamp, Wolfgang
Blackshear, Sam
Park, Junkil
Zohar, Yoni
Barrett, Clark
Dill, David L.
The Move Prover
title The Move Prover
title_full The Move Prover
title_fullStr The Move Prover
title_full_unstemmed The Move Prover
title_short The Move Prover
title_sort move prover
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363214/
http://dx.doi.org/10.1007/978-3-030-53288-8_7
work_keys_str_mv AT zhongjingyiemma themoveprover
AT cheangkevin themoveprover
AT qadeershaz themoveprover
AT grieskampwolfgang themoveprover
AT blackshearsam themoveprover
AT parkjunkil themoveprover
AT zoharyoni themoveprover
AT barrettclark themoveprover
AT dilldavidl themoveprover
AT zhongjingyiemma moveprover
AT cheangkevin moveprover
AT qadeershaz moveprover
AT grieskampwolfgang moveprover
AT blackshearsam moveprover
AT parkjunkil moveprover
AT zoharyoni moveprover
AT barrettclark moveprover
AT dilldavidl moveprover

Ejemplares similares