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