“The Move Prover” by Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, and David L. Dill. In Proceedings of the 32^nd International Conference on Computer Aided Verification (CAV '20), (Shuvendu K. Lahiri and Chao Wang, eds.), July 2020, pp. 137-150.
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.
BibTeX entry:
@inproceedings{ZCQ+20,
author = {Jingyi Emma Zhong and Kevin Cheang and Shaz Qadeer and
Wolfgang Grieskamp and Sam Blackshear and Junkil Park and Yoni
Zohar and Clark Barrett and David L. Dill},
editor = {Shuvendu K. Lahiri and Chao Wang},
title = {The Move Prover},
booktitle = {Proceedings of the {\it 32^{nd}} International Conference
on Computer Aided Verification (CAV '20)},
series = {Lecture Notes in Computer Science},
volume = {12224},
pages = {137--150},
publisher = {Springer International Publishing},
month = jul,
year = {2020},
isbn = {978-3-030-53288-8},
url = {http://theory.stanford.edu/~barrett/pubs/ZCQ+20.pdf}
}
(This webpage was created with bibtex2web.)