, The dao attacked: Code issue leads to $60 million ether theft -coindesk

, Ethereum white paper-a next generation smart contract and decentralized application platformvitalik-buterin, 2019.

F. , A higher-order effectful language designed for program verification, 2019.

, Known attacks -ethereum smart contract best practices

, Learn vyper in y minutes

, Vyper%20lets%20you%20program%20on,requiring%20centralized%20or%20trusted%20parties. &targetText=Like%20objects%20in%20OOP%2C%20each,functions%2C%20and%20common%20data% 20types, 2019.

, Model checking overview

. Vyper--vyper-documentation,

, Welcome! -the coq proof assistant

, Xacml 3.0 xacml:policy -complete documentation and samples, 2019.

T. Abdellatif and K. Brousmiche, Formal verification of smart contracts based on users and blockchain behaviors models, 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp.1-5, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01760787

S. Amani, M. Bégel, M. Bortin, and M. Staples, Towards verifying ethereum smart contract bytecode in isabelle/hol, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.66-77, 2018.

N. Atzei, M. Bartoletti, and T. Cimoli, A survey of attacks on ethereum smart contracts, IACR Cryptology ePrint Archive, p.1007, 2016.

X. Bai, Z. Cheng, Z. Duan, and K. Hu, Formal modeling and verification of smart contracts, Proceedings of the 2018 7th International Conference on Software and Computer Applications, pp.322-326, 2018.

K. Bhargavan, N. Swamy, S. Zanella-béguelin, A. Delignat-lavaud, C. Fournet et al., Formal verification of smart contracts: Short paper, Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security -PLAS'16, pp.91-96
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

J. Ellul and G. Pace, Runtime verification of ethereum smart contracts, 14th European Dependable Computing Conference (EDCC), pp.158-163, 2018.

S. Grossman, I. Abraham, G. Golan-gueta, Y. Michalevsky, N. Rinetzky et al., Online detection of effectively callback free objects with applications to smart contracts, Proceedings of the ACM on Programming Languages, vol.2, p.48, 2017.

E. Hildenbrandt, M. Saxena, N. Rodrigues, X. Zhu, P. Daian et al., Kevm: A complete formal semantics of the ethereum virtual machine, 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp.204-217, 2018.

A. Imeri, N. Agoulmine, and D. Khadraoui, A secure and smart environment for the transportation of dangerous goods by using blockchain and iot devices, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02439984

S. Kalra, S. Goel, M. Dhawan, and S. Sharma, Zeus: Analyzing safety of smart contracts, NDSS, 2018.

A. Kolluri, I. Nikolic, I. Sergey, A. Hobor, and P. Saxena, Exploiting the laws of order in smart contracts, Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.363-373, 2019.

L. Luu, D. Chu, H. Olickel, P. Saxena, and A. Hobor, Making smart contracts smarter, Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pp.254-269, 2016.

D. Magazzeni, P. Mcburney, and W. Nash, Validation and verification of smart contracts: A research agenda, vol.50, pp.50-57

A. Mavridou and A. Laszka, Designing secure ethereum smart contracts: A finite state machine based approach, International Conference on Financial Cryptography and Data Security, pp.523-540, 2018.

E. Mik, Smart contracts: terminology, technical limitations and real world complexity. Law, Innovation and Technology, vol.9, pp.269-300, 2017.

E. Mikk, Y. Lakhnech, M. Siegel, and G. J. Holzmann, Implementing statecharts in promela/spin, Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp.90-101, 1998.

Z. Nehai, P. Piriou, and F. Daumas, Model-checking of smart contracts
URL : https://hal.archives-ouvertes.fr/hal-02103511

I. Sergey, A. Kumar, and A. Hobor, Scilla: a smart contract intermediate-level language, 2018.

P. Tsankov, A. Dan, D. Drachsler-cohen, A. Gervais, F. Buenzli et al., Securify: Practical security analysis of smart contracts, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp.67-82, 2018.

X. Xu, I. Weber, M. Staples, L. Zhu, J. Bosch et al., A taxonomy of blockchain-based systems for architecture design, 2017 IEEE International Conference on, pp.243-252, 2017.

Z. Yang and H. Lei, Formal process virtual machine for smart contracts verification, 2018.

Z. Zheng, S. Xie, H. Dai, and H. Wang, Blockchain challenges and opportunities: A survey, 2016.