PV3 Move Proverchecks user-specified properties of Move smart contracts

Application domain/field

Type of tool

Auto-active verifier/deductive verifier

Expected input

Move source code annotated with specifications (pre-/postconditions).

Format:

Expected output

Whether the specification holds or some kind of source-level diagnosis/error.

Internals

The Move Prover translates annotated Move source code to the Boogie intermediate language. Boogie then generates an SMT formula which can be checked using an SMT solver such as Z3 or CVC4. "Move" is a language for implementing transactions, i.e. smart contracts, on the Libra blockchain. The Move Prover seems to be an auto-active verifier though this is not mentioned in the paper.
Smart contract

Links

Related papers

https://doi.org/10.1007/978-3-030-53288-8_7 (CAV '20)

Last publication date

14 July 2020

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.