\UseRawInputEncoding
\documentclass[runningheads,openbib]{llncs}

\input{prelude.tex}

%\renewcommand\UrlFont{\color{blue}\rmfamily}

\begin{document}

\author{
  David Dill \and Wolfgang Grieskamp(\Envelope)\thanks{\mailname~\email{wgrieskamp@gmail.com}} \and \\ Junkil
  Park \and Shaz Qadeer \and Meng Xu \and Emma Zhong
}

\institute{Novi Research, Meta Platforms, Menlo Park, USA}
  %\\\email{\{dill,wrwg,jkpark,shaz,mengxu,emmazjy\}@fb.com}}
\authorrunning{D. Dill, W. Grieskamp et. al.}

\title{Fast and Reliable Formal Verification of Smart Contracts with the Move
  Prover\thanks{To appear in TACAS'22. This is the extended version with
    appendices.}}

\maketitle
\begin{abstract}
  The Move Prover (\MVP) is a formal verifier for smart contracts written in the
  Move programming language. \MVP has an expressive specification language, and
  is fast and reliable enough that it can be run routinely by developers and in
  integration testing.  Besides the simplicity of smart contracts and the Move
  language, three implementation approaches are responsible for the practicality
  of \MVP: (1) an alias-free memory model, (2) fine-grained invariant checking,
  and (3) monomorphization.  The entirety of the Move code for the Diem
  blockchain has been extensively specified and can be completely verified by
  \MVP in a few minutes. Changes in the Diem framework must be successfully
  verified before being integrated into the open source repository on GitHub.
  \keywords{Smart contracts \and formal verification \and Move language \and
    Diem blockchain}
\end{abstract}


\input{intro.tex}
\input{move.tex}
\input{design.tex}
\input{analysis.tex}
\input{conclusion.tex}

%\vspace{-0.5ex}
\Paragraph{Acknowledgements}

This work would not have been possible without the many contributions of the
Move platform team and collaborators.  We specifically like to thank Bob Wilson,
Clark Barrett, Dario Russi, Jack Moffitt, Jake Silverman, Mathieu Baudet,
Runtian Zhou, Sam Blackshear, Tim Zakian, Todd Nowacki, Victor Gao, and Kevin
Cheang.

\appendix
\newpage
\input{function-injection-apx.tex}
\input{corrected_example-apx.tex}

\newpage
\bibliographystyle{splncs04}
\bibliography{biblio}

\vfill

{\small\medskip\noindent{\bf Open Access} This chapter is licensed under the terms of the Creative Commons\break Attribution 4.0 International License (\url{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.}

{\small \spaceskip .28em plus .1em minus .1em 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\break use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.}

\medskip\noindent\includegraphics{cc_by_4-0.eps}


\end{document}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: