Sidney Amani, Myriam Bégel, Maksym Bortin & Mark Staples (2018):
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL.
In: Proc. 7th International Conference on Certified Programs and Proofs (CPP),
doi:10.1145/3167084.
Danil Annenkov & Bas Spitters (2019):
Towards a Smart Contract Verification Framework in Coq.
In: Proc. 1st Workshop on Formal Methods for Blockchains (FMBC).
Karthukeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy & Santiago Zanella-Béguelin (2016):
Formal Verification of Smart Contracts.
In: Proc. 16th ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS),
pp. 91–96,
doi:10.1145/2993600.2993611.
Robert S. Boyer & J Strother Moore (1979):
A Computational Logic.
Academic Press,
doi:10.1016/C2013-0-10411-4.
Ting Chen, Xiaoqi Li, Xiapu Luo & Xiaosong Zhang (2017):
Under-Optimized Smart Contracts Devour Your Money.
In: Proc. 24th IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER),
pp. 442–446,
doi:10.1109/SANER.2017.7884650.
Sylvain Conchon, Alexandrina Korneva & Fatiha Zaïdi (2019):
Verifying Smart Contracts with Cubicle.
In: Proc. 1st Workshop on Formal Methods for Blockchains (FMBC).
Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth & Grigore Roşu (2017):
KEVM: A Complete Semantics of the Ethereum Virtual Machine.
Technical Report.
University of Illinois Urbana-Champaign.
http://hdl.handle.net/2142/97207.
Yoichi Hirai:
Formalization of Ethereum Virtual Machine in Lem.
https://github.com/pirapira/eth-isabelle.
Yoichi Hirai (2017):
Defining the Ethereum Virtual Machine for Interactive Theorem Provers.
In: Proc. 1st Workshop on Trusted Smart Contracts (WTSC),
LNCS,
doi:10.1007/978-3-319-70278-0_33.
Sukrit Kalra, Seep Goel, Mohan Dhawan & Subodh Sharma (2018):
ZEUS: Analyzing Safety of Smart Contracts.
In: Proc. 25th Annual Network and Distributed System Security Symposium (NDSS),
doi:10.14722/ndss.2018.23082.
Matt Kaufmann & J Strother Moore:
The ACL2 Theorem Prover: Web Site.
http://www.cs.utexas.edu/users/moore/acl2.
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena & Aquinas Hobor (2016):
Making Smart Contracts Smarter.
In: Proc. 23rd Conference on Computer and Communication Security (CCS),
pp. 254–269,
doi:10.1145/2976749.2978309.
Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi & Natasha Sharygina (2018):
Computing Exact Worst-Case Gas Consumption for Smart Contracts.
In: Proc. 8th International Symposium on Leveraging Applications of Formal Methods (ISoLA),
LNCS 11247,
pp. 450–465,
doi:10.1007/978-3-030-03427-6_33.
Zeinab Nehaï & François Bobot (2019):
Deductive Proof of Industrial Smart Contracts Using Why3.
In: Proc. 1st Workshop on Formal Methods for Blockchains (FMBC).
Ivica Nikoli\'c, Aashish Kolluri, Ilya Sergey, Prateek Saxena & Aquinas Hobor (2018):
Finding the Greedy, Prodigal, and Suicidal Contracts at Scale.
In: Proc. 34th Annual Computer Security Applications Conference (ACSAC),
pp. 653–663.
The ACL2 Community:
The ACL2 Theorem Prover and Community Books: Documentation.
http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual.
The ACL2 Community:
The ACL2 Theorem Prover and Community Books: Source Code.
http://github.com/acl2/acl2.
The Ethereum Community:
The Ethereum Test Suite.
https://github.com/ethereum/tests.
The Ethereum Community:
The Ethereum Web Site.
https://ethereum.org.
The Ethereum Community:
The Ethereum Wiki.
https://github.com/ethereum/wiki.
The KEVM Team:
JelloPaper: Human Readable Semantics of EVM in K.
https://jellopaper.org.
Gavin Wood:
Ethereum: A Secure Decentralized Generalised Transaction Ledger.
https://github.com/ethereum/yellowpaper.
eptcs@eptcs.org