P. Asirelli, M. H. Ter-beek, A. Fantechi, and S. Gnesi, A model-checking tool for families of services, Proc. of Joint 13th IFIP WG, vol.6
URL : https://hal.archives-ouvertes.fr/hal-01583318

, Int. Conf. on Formal Techniques for Distributed Systems, vol.6722, pp.44-58, 2011.

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Gollamudi, G. Gonthier et al., Formal verification of smart contracts: Short paper, Proc. of Programming Languages and Analysis for Security, pp.91-96, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01400469

G. Bigi, A. Bracciali, G. Meacci, and E. Tuosto, Validation of decentralised smart contracts through game theory and formal methods, Programming Languages with Applications to Biology and Security, vol.9465, pp.142-161, 2015.

K. Chatterjee, Y. Amir-kafshdar-goharshady, and . Velner, Quantitative analysis of smart contracts, Proc. of ESOP, vol.10801, pp.739-767, 2018.

S. Demri, Linear-time temporal logics with presburger constraints: an overview, Journal of Applied Non-Classical Logics, vol.16, issue.3-4, pp.311-348, 2006.

, Ethereum's white paper, 2014.

, Ethereum Foundation, 2019.

V. Ganesh, S. Berezin, and D. L. Dill, Deciding presburger arithmetic by model checking and comparisons with other methods, Formal Methods in Computer-Aided Design, pp.171-186, 2002.

C. Haase, A survival guide to presburger arithmetic, ACM SIGLOG News, vol.5, issue.3, pp.67-82, 2018.

L. Luu, D. Chu, H. Olickel, P. Saxena, and A. Hobor, Making smart contracts smarter, Proc. of the Conference on Computer and Communications Security, pp.254-269, 2016.

B. Mueller, Smashing Ethereum smart contracts for fun and real profit, HITB SECCONF Amsterdam, 2018.

A. Pnueli, The temporal logic of programs, Proc. of Symposium on Foundations of Computer Science, pp.46-57, 1977.

J. Pope, Formalizing constructive quantifier elimination in Agda, Proceedings. of MSFP@FSCD, vol.275, pp.2-17, 2018.

S. Ocamlpro, Welcome to Liquidity's documentation!, 2019.

D. Siegel, Understanding the dao attack, vol.13, 2016.