%% This BibTeX bibliography file was created using BibDesk.
%% https://bibdesk.sourceforge.io/

%% Created for jkpark at 2021-10-06 10:38:07 -0700


%% Saved with string encoding Unicode (UTF-8)

@article{FULL_VERSION,
  author    = {David L. Dill and
               Wolfgang Grieskamp and
               Junkil Park and
               Shaz Qadeer and
               Meng Xu and
               Jingyi Emma Zhong},
  title     = {Fast and Reliable Formal Verification of Smart Contracts with the
               Move Prover (extended version)},
  journal   = {CoRR},
  volume    = {abs/2110.08362},
  year      = {2021},
  url       = {https://arxiv.org/abs/2110.08362},
  eprinttype = {arXiv},
  eprint    = {2110.08362},
  timestamp = {Fri, 22 Oct 2021 13:33:09 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2110-08362.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@article{liu2019survey,
	author = {Liu, Jing and Liu, Zhentian},
	date-added = {2021-10-06 10:38:04 -0700},
	date-modified = {2021-10-06 10:38:04 -0700},
	journal = {IEEE Access},
	pages = {77894--77904},
	publisher = {IEEE},
	title = {A survey on security verification of blockchain smart contracts},
	volume = {7},
	year = {2019}}

@inproceedings{miller2018smart,
	author = {Miller, Andrew and Cai, Zhicheng and Jha, Somesh},
	booktitle = {International Symposium on Leveraging Applications of Formal Methods},
	date-added = {2021-10-06 10:37:12 -0700},
	date-modified = {2021-10-06 10:37:12 -0700},
	organization = {Springer},
	pages = {280--299},
	title = {Smart contracts and opportunities for formal methods},
	year = {2018}}

@inproceedings{MOVE_PROVER,
	author = {Zhong, Jingyi Emma and Cheang, Kevin and Qadeer, Shaz and Grieskamp, Wolfgang and Blackshear, Sam and Park, Junkil and Zohar, Yoni and Barrett, Clark and Dill, David L.},
	booktitle = {Computer Aided Verification},
	editor = {Lahiri, Shuvendu K. and Wang, Chao},
	pages = {137--150},
	publisher = {Springer International Publishing},
	title = {{The Move Prover}},
	year = {2020}}

@misc{DIEM,
	author = {{The Diem Association}},
	title = {{An Introduction to Diem}},
	url = {https://www.diem.com/en-us/},
	bdsk-url-1 = {https://www.diem.com/en-us/},
	year = {2019}}

@incollection{BORROW_SEM,
	author = {Dave Clarke and Johan {\"{O}}stlund and Ilya Sergey and Tobias Wrigstad},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/series/lncs/ClarkeOSW13.bib},
	booktitle = {Aliasing in Object-Oriented Programming. Types, Analysis and Verification},
	doi = {10.1007/978-3-642-36946-9\_3},
	editor = {Dave Clarke and James Noble and Tobias Wrigstad},
	pages = {15--58},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	timestamp = {Tue, 14 May 2019 10:00:55 +0200},
	title = {Ownership Types: {A} Survey},
	NOurl = {https://doi.org/10.1007/978-3-642-36946-9\_3},
	volume = {7850},
	year = {2013},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-36946-9%5C_3}}

@misc{UNAVAILABLE_BORROW_CHECKER,
	author = {Sam Blackshear and Todd Nowacki and Shaz Qadeer and John Mitchell},
	title = {The Move Borrow Checker},
	url = {TBD},
	year = {2021},
	bdsk-url-1 = {TBD}}

@article{RUST_SECURE,
	address = {New York, NY, USA},
	articleno = {66},
	author = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
	doi = {10.1145/3158154},
	issue_date = {January 2018},
	journal = {Proc. ACM Program. Lang.},
	keywords = {logical relations, separation logic, type systems, Rust, concurrency},
	month = dec,
	number = {POPL},
	numpages = {34},
	publisher = {Association for Computing Machinery},
	title = {RustBelt: Securing the Foundations of the Rust Programming Language},
	url = {https://doi.org/10.1145/3158154},
	volume = {2},
	year = {2017},
	bdsk-url-1 = {https://doi.org/10.1145/3158154}}

@article{DESIGN_BY_CONTRACT,
	address = {Washington, DC, USA},
	author = {Meyer, Bertrand},
	doi = {10.1109/2.161279},
	issn = {0018-9162},
	issue_date = {October 1992},
	journal = {Computer},
	month = oct,
	number = {10},
	numpages = {12},
	pages = {40--51},
	publisher = {IEEE Computer Society Press},
	title = {Applying "Design by Contract"},
	NOurl = {https://doi.org/10.1109/2.161279},
	volume = {25},
	year = {1992},
	bdsk-url-1 = {https://doi.org/10.1109/2.161279}}

@article{CONTRACT_VERIFICATION,
	author = {Palina Tolmach and Yi Li and Shang{-}Wei Lin and Yang Liu and Zengxiang Li},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/corr/abs-2008-02712.bib},
	eprint = {2008.02712},
	eprinttype = {arXiv},
	journal = {CoRR},
	timestamp = {Wed, 07 Jul 2021 10:04:24 +0200},
	title = {A Survey of Smart Contract Formal Specification and Verification},
	url = {https://arxiv.org/abs/2008.02712},
	volume = {abs/2008.02712},
	year = {2020},
	bdsk-url-1 = {https://arxiv.org/abs/2008.02712}}

@article{DAFNY,
	address = {Los Alamitos, CA, USA},
	author = {K. M. Leino},
	doi = {10.1109/MS.2017.4121212},
	issn = {1937-4194},
	journal = {IEEE Software},
	keywords = {formal verification;software reliability;software development;encoding;cognition},
	month = {nov},
	number = {06},
	pages = {94-97},
	publisher = {IEEE Computer Society},
	title = {Accessible Software Verification with Dafny},
	volume = {34},
	year = {2017},
	bdsk-url-1 = {https://doi.org/10.1109/MS.2017.4121212}}

@inbook{SPECSHARP,
	abstract = {The Spec{\#} programming system [4] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer assumptions explicit. Using modern technology, we propose the use of tools to enforce the specifications. To increase its chances of having impact, we want to design the system so that it can be widely adopted.},
	address = {Berlin, Heidelberg},
	author = {Barnett, Mike and DeLine, Robert and F{\"a}hndrich, Manuel and Jacobs, Bart and Leino, K. Rustan M. and Schulte, Wolfram and Venter, Herman},
	booktitle = {Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions},
	isbn = {978-3-540-69149-5},
	pages = {144--152},
	publisher = {Springer Berlin Heidelberg},
	title = {The Spec{\#} Programming System: Challenges and Directions},
	url = {https://doi.org/10.1007/978-3-540-69149-5_16},
	year = {2008},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-540-69149-5_16}}

@inproceedings{REENTRANCE,
	author = {Fatima Samreen, Noama and Alalfi, Manar H.},
	booktitle = {2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE)},
	pages = {22-29},
	title = {Reentrancy Vulnerability Identification in Ethereum Smart Contracts},
	year = {2020}}

@misc{SOLIDITY_EVENTS,
	archiveprefix = {arXiv},
	author = {{\'A}kos Hajdu and Dejan Jovanovi{\'c} and Gabriela Ciocarlie},
	eprint = {2005.10382},
	primaryclass = {cs.PL},
	title = {Formal Specification and Verification of Solidity Contracts with Events},
	year = {2020}}

@misc{OLD_MOVE_LANG,
	author = {Sam Blackshear and Evan Cheng and David L. Dill and Victor Gao and Ben Maurer and Todd Nowacki and Alistair Pott and Shaz Qadeer and Rain and Dario Russi and Stephane Sezer and Tim Zakian and Runtian Zho},
	title = {{Move: A Language With Programmable Resources}},
	url = {https://developers.libra.org/docs/move-paper},
	year = {2019},
	bdsk-url-1 = {https://developers.libra.org/docs/move-paper}}

@misc{DIEM_FRAMEWORK,
	author = {{The Diem Association}},
	title = {{The Diem Framework}},
	url = {https://github.com/diem/diem/tree/release-1.5/diem-move/diem-framework},
	year = {2020},
	bdsk-url-1 = {https://github.com/diem/diem/tree/release-1.5/diem-move/diem-framework}}

@inproceedings{LINEAR_TYPES,
	author = {Philip Wadler},
	booktitle = {PROGRAMMING CONCEPTS AND METHODS},
	publisher = {North},
	title = {Linear Types Can Change the World!},
	year = {1990}}

@article{RUST_TYPES,
	archiveprefix = {arXiv},
	author = {Aaron Weiss and Daniel Patterson and Nicholas D. Matsakis and Amal Ahmed},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/corr/abs-1903-00982.bib},
	eprint = {1903.00982},
	journal = {CoRR},
	timestamp = {Sat, 30 Mar 2019 19:27:21 +0100},
	title = {Oxide: The Essence of Rust},
	url = {http://arxiv.org/abs/1903.00982},
	volume = {abs/1903.00982},
	year = {2019},
	bdsk-url-1 = {http://arxiv.org/abs/1903.00982}}

@misc{MOVE_LANG,
	author = {{The Move Team}},
	title = {{The Move Programming Language}},
	url = {https://diem.github.io/move},
	year = {2020},
	bdsk-url-1 = {https://diem.github.io/move},
}

@misc{MOVE_SPEC_LANG_DEF,
	author = {{The Move Team}},
	title = {{The Move Specification Language}},
	url = {https://github.com/diem/diem/blob/release-1.5/language/move-prover/doc/user/spec-lang.md},
	year = 2020,
	bdsk-url-1 = {https://github.com/diem/diem/blob/release-1.5/language/move-prover/doc/user/spec-lang.md}
}

@misc{CVC,
	author = {{The CVC Team}},
	title = {{CVC5}},
	url = {https://github.com/cvc5/cvc5},
	bdsk-url-1 = {https://github.com/cvc5/cvc5}}

@inproceedings{BUTTERFLY,
	author        = "K. Rustan M. Leino and Clément Pit-Claudel",
	booktitle     = "{Proceedings of the 28th International Conference on Computer Aided Verification, Part I}",
	doi           = {10.1007/978-3-319-41528-4\_20},
	isbn          = "978-3-319-41527-7",
	pages         = "361--381",
	publisher     = "{Springer}",
	title         = "{Trigger Selection Strategies to Stabilize Program Verifiers}",
	year          = 2016,
}


@misc{blackshear2020resources,
	archiveprefix = {arXiv},
	author = {Sam Blackshear and David L. Dill and Shaz Qadeer and Clark W. Barrett and John C. Mitchell and Oded Padon and Yoni Zohar},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/corr/abs-2004-05106.bib},
	eprint = {2004.05106},
	journal = {CoRR},
	timestamp = {Tue, 14 Apr 2020 16:40:34 +0200},
	title = {Resources: {A} Safe Language Abstraction for Money},
	url = {https://arxiv.org/abs/2004.05106},
	volume = {abs/2004.05106},
	year = {2020},
	bdsk-url-1 = {https://arxiv.org/abs/2004.05106}}

@article{prusti,
	author = {Vytautas Astrauskas and Peter M{\"{u}}ller and Federico Poli and Alexander J. Summers},
	journal = {{PACMPL}},
	number = {{OOPSLA}},
	pages = {147:1--147:30},
	title = {Leveraging rust types for modular specification and verification},
	volume = {3},
	year = {2019}}

@inproceedings{SMTLib2010,
	author = {Clark Barrett and Aaron Stump and Cesare Tinelli},
	booktitle = {Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)},
	editor = {A.~Gupta and D.~Kroening},
	title = {{The SMT-LIB Standard: Version 2.0}},
	year = 2010}

@misc{libra_blockchain_white,
	author = {Zachary Amsden and Ramnik Arora and Shehar Bano and Mathieu Baudet and Sam Blackshear and Abhay Bothra and George Cabrera and Christian Catalini and Konstantinos Chalkias and Evan Cheng and Avery Ching and Andrey Chursin and George Danezis and Gerardo Di Giacomo and David L. Dill and Hui Ding and Nick Doudchenko and Victor Gao and Zhenhuan Gao and Fran{\c c}ois Garillot and Michael Gorven and Philip Hayes and J. Mark Hou and Yuxuan Hu and Kevin Hurley and Kevin Lewi and Chunqi Li and Zekun Li and Dahlia Malkhi and Sonia Margulis and Ben Maurer and Payman Mohassel and Ladi de Naurois and Valeria Nikolaenko and Todd Nowacki and Oleksandr Orlov and Dmitri Perelman and Alistair Pott and Brett Proctor and Shaz Qadeer and Rain and Dario Russi and Bryan Schwab and Stephane Sezer and Alberto Sonnino and Herman Venter and Lei Wei and Nils Wernerfelt and Brandon Williams and Qinfan Wu and Xifan Yan and Tim Zakian and Runtian Zhou},
	howpublished = {\url{https://developers.libra.org/docs/the-libra-blockchain-paper}},
	title = {The {L}ibra {B}lockchain},
	year = {2019}}

@inproceedings{smack,
	author = {Marek S. Baranowski and Shaobo He and Zvonimir Rakamaric},
	booktitle = {{ATVA}},
	pages = {528--535},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Verifying Rust Programs with {SMACK}},
	volume = {11138},
	year = {2018}}

@inproceedings{nopanic,
	author = {Marcus Lindner and Jorge Aparicius and Per Lindgren},
	booktitle = {{INDIN}},
	pages = {108--114},
	publisher = {{IEEE}},
	title = {No Panic! Verification of Rust Programs by Symbolic Execution},
	year = {2018}}

@inproceedings{crust,
	author = {John Toman and Stuart Pernsteiner and Emina Torlak},
	booktitle = {{ASE}},
	pages = {75--80},
	publisher = {{IEEE} Computer Society},
	title = {Crust: {A} Bounded Verifier for Rust {(N)}},
	year = {2015}}

@incollection{viper,
	author = {Peter M{\"{u}}ller and Malte Schwerhoff and Alexander J. Summers},
	booktitle = {Dependable Software Systems Engineering},
	pages = {104--125},
	publisher = {{IOS} Press},
	series = {{NATO} Science for Peace and Security Series - {D:} Information and Communication Security},
	title = {Viper: {A} Verification Infrastructure for Permission-Based Reasoning},
	volume = {50},
	year = {2017}}

@misc{libra_consensus_white,
	author = {Mathieu Baudet and Avery Ching and Andrey Chursin and George Danezis and Fran{\c c}ois Garillot and Zekun Li and Dahlia Malkhi and Oded Naor and Dmitri Perelman and Alberto Sonnino},
	howpublished = {\url{https://developers.libra.org/docs/state-machine-replication-paper}},
	title = {State Machine Replication in the {L}ibra {B}lockchain},
	year = {2019}}

@misc{libra_whitepaper,
	author = {{The Libra Association}},
	howpublished = {\url{https://libra.org/en-us/whitepaper}},
	title = {An {I}ntroduction to {L}ibra},
	year = {2019}}

@misc{libra_association,
	author = {{The Libra Association}},
	howpublished = {\url{https://libra.org/en-us/association-council-principles}},
	title = {The {L}ibra {A}ssociation}}

@misc{libra_transition,
	author = {Shehar Bano and Christian Catalini and George Danezis and Nick Doudchenko and Ben Maurer and Alberto Sonnino and Nils Wernerfelt},
	howpublished = {\url{https://libra.org/permissionless-blockchain}},
	title = {Moving Toward Permissionless Consensus}}

@article{Herlihy2019,
	acmid = {3209623},
	address = {New York, NY, USA},
	author = {Herlihy, Maurice},
	doi = {10.1145/3209623},
	issn = {0001-0782},
	issue_date = {February 2019},
	journal = {Commun. ACM},
	month = jan,
	number = {2},
	numpages = {8},
	pages = {78--85},
	publisher = {ACM},
	title = {Blockchains from a Distributed Computing Perspective},
	url = {http://doi.acm.org/10.1145/3209623},
	volume = {62},
	year = {2019},
	bdsk-url-1 = {http://doi.acm.org/10.1145/3209623},
	bdsk-url-2 = {https://doi.org/10.1145/3209623}}

@misc{JPMcoin,
	author = {R. Armstrong},
	howpublished = {Financial Times},
	month = {February},
	title = {JPMorgan plan to coin it on the blockchain},
	url = {https://www.ft.com/content/0bafd9d6-307e-11e9-8744-e7016697f225},
	year = {2019},
	bdsk-url-1 = {https://www.ft.com/content/0bafd9d6-307e-11e9-8744-e7016697f225}}

@misc{HBR-global-supply-chain,
	author = {M.J. Casey and P. Wong},
	howpublished = {Harvard Business Review},
	month = {March},
	title = {Global Supply Chains Are About to Get Better, Thanks to Blockchain},
	year = {2017}}

@inproceedings{DBLP:conf/ccs/BhargavanDFGGKK16,
	author = {Karthikeyan Bhargavan and Antoine Delignat{-}Lavaud and C{\'{e}}dric Fournet and Anitha Gollamudi and Georges Gonthier and Nadim Kobeissi and Natalia Kulatova and Aseem Rastogi and Thomas Sibut{-}Pinote and Nikhil Swamy and Santiago Zanella B{\'{e}}guelin},
	booktitle = {PLAS@CCS},
	pages = {91--96},
	publisher = {{ACM}},
	title = {Formal Verification of Smart Contracts: Short Paper},
	year = {2016}}

@misc{solidity,
	author = {Ethereum Foundation},
	title = {Solidity Documentation},
	url = {http://solidity.readthedocs.io},
	year = {2018},
	bdsk-url-1 = {http://solidity.readthedocs.io}}

@misc{mythril,
	author = {{ConsenSys}},
	title = {{Mythril Classic: Security analysis tool for Ethereum smart contracts}},
	url = {https://github.com/skylightcyber/mythril-classic},
	bdsk-url-1 = {https://github.com/skylightcyber/mythril-classic}}

@inproceedings{post2018,
	author = {Ilya Grishchenko and Matteo Maffei and Clara Schneidewind},
	booktitle = {{POST}},
	pages = {243--269},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Semantic Framework for the Security Analysis of Ethereum Smart Contracts},
	volume = {10804},
	year = {2018}}

@article{concert,
	author = {Danil Annenkov and Bas Spitters},
	journal = {CoRR},
	title = {Towards a Smart Contract Verification Framework in Coq},
	volume = {abs/1907.10674},
	year = {2019}}

@article{fspvme,
	author = {Zheng Yang and Hang Lei},
	journal = {CoRR},
	title = {Formal Process Virtual Machine for Smart Contracts Verification},
	volume = {abs/1805.00808},
	year = {2018}}

@article{fether,
	author = {Zheng Yang and Hang Lei},
	journal = {{IEEE} Access},
	pages = {37770--37791},
	title = {FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq},
	volume = {7},
	year = {2019}}

@other{coqref,
	author = {{The Coq development team}},
	title = {The Coq Proof Assistant Reference Manual Version 8.9},
	url = {https://coq.inria.fr/distrib/current/refman/},
	year = {2019},
	bdsk-url-1 = {https://coq.inria.fr/distrib/current/refman/}}

@inproceedings{dm4all,
	author = {Kenji Maillard and Danel Ahman and Robert Atkey and Guido Mart\'inez and Catalin Hritcu and Exequiel Rivas and \'Eric Tanter},
	booktitle = {24th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
	title = {Dijkstra Monads for All},
	url = {https://arxiv.org/abs/1903.01237},
	year = {2019},
	bdsk-url-1 = {https://arxiv.org/abs/1903.01237}}

@article{reachabilitylogic,
	author = {Andrei Stefanescu and \c{S}tefan Ciob\^ac\u{a} and Radu Mereuta and Brandon M. Moore and Traian{-}Florin Serbanuta and Grigore Rosu},
	journal = {Logical Methods in Computer Science},
	number = {2},
	title = {All-Path Reachability Logic},
	volume = {15},
	year = {2019}}

@article{kay,
	author = {Grigore Rosu and Traian{-}Florin Serbanuta},
	journal = {J. Log. Algebr. Program.},
	number = {6},
	pages = {397--434},
	title = {An overview of the {K} semantic framework},
	volume = {79},
	year = {2010}}

@inproceedings{kevm,
	author = {Everett Hildenbrandt and Manasvi Saxena and Nishant Rodrigues and Xiaoran Zhu and Philip Daian and Dwight Guth and Brandon M. Moore and Daejun Park and Yi Zhang and Andrei Stefanescu and Grigore Rosu},
	booktitle = {{CSF}},
	pages = {204--217},
	publisher = {{IEEE} Computer Society},
	title = {{KEVM:} {A} Complete Formal Semantics of the Ethereum Virtual Machine},
	year = {2018}}

@inproceedings{securify,
	author = {Petar Tsankov and Andrei Marian Dan and Dana Drachsler{-}Cohen and Arthur Gervais and Florian B{\"{u}}nzli and Martin T. Vechev},
	booktitle = {{ACM} Conference on Computer and Communications Security},
	pages = {67--82},
	publisher = {{ACM}},
	title = {Securify: Practical Security Analysis of Smart Contracts},
	year = {2018}}

@inproceedings{maian,
	author = {Ivica Nikolic and Aashish Kolluri and Ilya Sergey and Prateek Saxena and Aquinas Hobor},
	booktitle = {{ACSAC}},
	pages = {653--663},
	publisher = {{ACM}},
	title = {Finding The Greedy, Prodigal, and Suicidal Contracts at Scale},
	year = {2018}}

@inproceedings{oyente,
	author = {Loi Luu and Duc{-}Hiep Chu and Hrishi Olickel and Prateek Saxena and Aquinas Hobor},
	booktitle = {{ACM} Conference on Computer and Communications Security},
	pages = {254--269},
	publisher = {{ACM}},
	title = {Making Smart Contracts Smarter},
	year = {2016}}

@inproceedings{smtalt18,
	author = {Leonardo Alt and Christian Reitwie{\ss}ner},
	booktitle = {ISoLA {(4)}},
	pages = {376--388},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {{SMT-Based Verification of Solidity Smart Contracts}},
	volume = {11247},
	year = {2018}}

@article{solcverify,
	author = {{\'{A}}kos Hajdu and Dejan Jovanovic},
	journal = {CoRR},
	title = {solc-verify: {A} Modular Verifier for Solidity Smart Contracts},
	volume = {abs/1907.04262},
	year = {2019}}

@inproceedings{corral,
	author = {Akash Lal and Shaz Qadeer and Shuvendu K. Lahiri},
	booktitle = {{CAV}},
	pages = {427--443},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Solver for Reachability Modulo Theories},
	volume = {7358},
	year = {2012}}

@article{verisol,
	author = {Shuvendu K. Lahiri and Shuo Chen and Yuepeng Wang and Isil Dillig},
	journal = {CoRR},
	title = {Formal Specification and Verification of Smart Contracts for Azure Blockchain},
	volume = {abs/1812.08829},
	year = {2018}}

@article{scilla,
	author = {Ilya Sergey and Vaivaswatha Nagaraj and Jacob Johannsen and Amrit Kumar and Anton Trunov and Ken Chan Guan Hao},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/journals/pacmpl/SergeyNJ0TH19},
	doi = {10.1145/3360611},
	journal = {{PACMPL}},
	number = {{OOPSLA}},
	pages = {185:1--185:30},
	timestamp = {Mon, 21 Oct 2019 15:15:21 +0200},
	title = {Safer smart contract programming with Scilla},
	url = {https://doi.org/10.1145/3360611},
	volume = {3},
	year = {2019},
	bdsk-url-1 = {https://doi.org/10.1145/3360611}}

@misc{erc20,
	author = {Vitalik Buterin and Fabian Vogelsteller},
	title = {ERC20 Token Standard},
	url = {https://theethereum.wiki/w/index.php/ERC20_Token_Standard},
	year = {2015},
	bdsk-url-1 = {https://theethereum.wiki/w/index.php/ERC20_Token_Standard}}

@misc{re_dao,
	author = {Vitalik Buterin},
	title = {Critical update re {DAO}},
	url = {https://ethereum.github.io/blog/2016/06/17/critical-update-re-dao-vulnerability},
	year = {2016},
	bdsk-url-1 = {https://ethereum.github.io/blog/2016/06/17/critical-update-re-dao-vulnerability}}

@misc{sm,
	author = {{Synthetic Minds Blog}},
	title = {Verifying Smart Contracts in The Move Language},
	url = {https://synthetic-minds.com/pages/blog/blog-2019-09-11.html},
	year = {2019},
	bdsk-url-1 = {https://synthetic-minds.com/pages/blog/blog-2019-09-11.html}}

@inproceedings{DBLP:conf/esop/HajduJ20,
	author = {{\'{A}}kos Hajdu and Dejan Jovanovic},
	booktitle = {{ESOP}},
	pages = {224--250},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {{SMT-Friendly Formalization of the Solidity Memory Model}},
	volume = {12075},
	year = {2020}}

@misc{parity_hack,
	author = {Palladino, Santiago},
	title = {The {P}arity wallet hack explained},
	url = {https://blog. zeppelin. solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7},
	year = {2017},
	bdsk-url-1 = {https://blog.%20zeppelin.%20solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7}}

@article{nakamoto,
	author = {Satoshi Nakamoto},
	title = {Bitcoin: A peer-to-peer electronic cash system},
	url = {http://bitcoin.org/bitcoin.pdf},
	year = {2008},
	bdsk-url-1 = {http://bitcoin.org/bitcoin.pdf}}

@misc{bitcoin_script,
	author = {Bitcoin Wiki},
	title = {Bitcoin Script},
	url = {https://en.bitcoin.it/wiki/Script},
	year = {online},
	bdsk-url-1 = {https://en.bitcoin.it/wiki/Script}}

@misc{simplicity,
	author = {Russell O'Connor},
	title = {Simplicity: A New Language for Blockchains},
	url = {https://blockstream.com/simplicity.pdf},
	year = {2017},
	bdsk-url-1 = {https://blockstream.com/simplicity.pdf}}

@article{ethereum,
	author = {Gavin Wood},
	title = {Ethereum: A secure decentralised generalised transaction ledger},
	url = {https://ethereum.github.io/yellowpaper/paper.pdf},
	year = {2014},
	bdsk-url-1 = {https://ethereum.github.io/yellowpaper/paper.pdf}}

@incollection{substructural_type_systems,
	author = {David Walker},
	booktitle = {Advanced Topics in Types and Programming Languages},
	chapter = {1},
	isbn = {0262162288},
	publisher = {The MIT Press},
	title = {Substructural Type Systems},
	year = {2004}}

@article{tal,
	author = {J. Gregory Morrisett and David Walker and Karl Crary and Neal Glew},
	journal = {{ACM} Trans. Program. Lang. Syst.},
	title = {From {S}ystem {F} to typed assembly language},
	year = {1999}}

@article{linear_logic,
	author = {Jean{-}Yves Girard},
	journal = {Theor. Comput. Sci.},
	title = {Linear Logic},
	year = {1987}}

@article{using_time,
	author = {Leslie Lamport},
	journal = {{ACM} Trans. Program. Lang. Syst.},
	title = {Using Time Instead of Timeout for Fault-Tolerant Distributed Systems},
	year = {1984}}

@book{jvm,
	author = {Tim Lindholm and Frank Yellin},
	publisher = {Addison-Wesley},
	title = {The {J}ava Virtual Machine Specification},
	year = {1997}}

@misc{clr,
	author = {Erik Meijer and Redmond Wa and John Gough},
	title = {Technical Overview of the Common Language Runtime},
	year = {2000}}

@misc{michelson,
	author = {Tezos Foundation},
	howpublished = {\url{http://tezos.gitlab.io/mainnet/whitedoc/michelson.html}},
	title = {Michelson: the language of Smart Contracts in Tezos},
	year = {2018}}

@misc{plutus,
	author = {IOHK Foundation},
	howpublished = {\url{https://testnet.iohkdev.io/plutus}},
	title = {Plutus: A Functional Contract Platform},
	year = {2019}}

@misc{agoric,
	author = {Agoric},
	url = {https://github.com/Agoric/SES},
	bdsk-url-1 = {https://github.com/Agoric/SES}}

@misc{github-libra,
	author = {Libra},
	url = {https://github.com/libra/libra},
	bdsk-url-1 = {https://github.com/libra/libra}}

@inproceedings{boogieIVL,
	address = {Berlin, Heidelberg},
	author = {Leino, K. Rustan M. and R{\"u}mmer, Philipp},
	booktitle = {TACAS},
	editor = {Esparza, Javier and Majumdar, Rupak},
	isbn = {978-3-642-12002-2},
	pages = {312--327},
	publisher = {Springer Berlin Heidelberg},
	title = {A Polymorphic Intermediate Verification Language: Design and Logical Encoding},
	year = {2010}}

@misc{thisisboogie2,
	author = {Leino, K. Rustan M.},
	note = {Manuscript KRML 178},
	title = {This is Boogie 2},
	url = {{https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/}},
	year = {2008},
	bdsk-url-1 = {%7Bhttps://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/%7D}}

@inproceedings{BL05,
	address = {New York, NY, USA},
	author = {Barnett, Mike and Leino, K. Rustan M.},
	booktitle = {Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering},
	doi = {10.1145/1108792.1108813},
	isbn = {1595932399},
	location = {Lisbon, Portugal},
	numpages = {6},
	pages = {82---87},
	publisher = {Association for Computing Machinery},
	title = {Weakest-Precondition of Unstructured Programs},
	year = {2005},
	bdsk-url-1 = {https://doi.org/10.1145/1108792.1108813}}

@inproceedings{boogie,
	author = {Barnett, Mike and Chang, Bor-Yuh Evan and DeLine, Robert and Jacobs, Bart and Leino, K Rustan M},
	booktitle = {International Symposium on Formal Methods for Components and Objects},
	organization = {Springer},
	pages = {364--387},
	title = {Boogie: A modular reusable verifier for object-oriented programs},
	year = {2005}}

@misc{boogie-github,
	title = {Boogie},
	url = {https://github.com/boogie-org/boogie},
	bdsk-url-1 = {https://github.com/boogie-org/boogie}}

@misc{pact,
	author = {Stuart Popejoy},
	howpublished = {\url{ http://kadena.io/docs/Kadena-PactWhitepaper.pdf}},
	title = {The Pact Smart-Contract Language},
	year = {2017}}

@article{tx_replay,
	author = {Muhammad Saad and Jeffrey Spaulding and Laurent Njilla and Charles A. Kamhoua and Sachin Shetty and DaeHun Nyang and Aziz Mohaisen},
	journal = {CoRR},
	title = {Exploring the Attack Surface of Blockchain: {A} Systematic Overview},
	year = {2019}}

@inproceedings{Jones-al:POPL79,
	author = {Jones, Neil D. and Muchnick, Steven S.},
	booktitle = {POPL},
	title = {Flow Analysis and Optimization of {LISP}-like Structures},
	year = {1979}}

@inproceedings{standard_ml90,
	author = {Robin Milner and Mads Tofte and Robert Harper},
	publisher = {{MIT} Press},
	title = {Definition of standard {ML}},
	year = {1990}}

@inproceedings{BartolettiZ18,
	author = {Massimo Bartoletti and Roberto Zunino},
	booktitle = {Proceedings of the {ACM} {SIGSAC} Conference on Computer and Communications Security},
	title = {BitML: {A} Calculus for {B}itcoin Smart Contracts},
	year = {2018}}

@inproceedings{CraryS15,
	author = {Karl Crary and Michael J. Sullivan},
	booktitle = {Proceedings of the {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation},
	title = {Peer-to-peer affine commitment using bitcoin},
	year = {2015}}

@article{szabo_smart_contracts,
	author = {Nick Szabo},
	journal = {First Monday},
	number = {9},
	title = {Formalizing and Securing Relationships on Public Networks},
	url = {https://ojphi.org/ojs/index.php/fm/article/view/548},
	volume = {2},
	year = {1997},
	bdsk-url-1 = {https://ojphi.org/ojs/index.php/fm/article/view/548}}

@inproceedings{MazurakZZ10,
	author = {Karl Mazurak and Jianzhou Zhao and Steve Zdancewic},
	booktitle = {Proceedings of the {ACM} {SIGPLAN} International Workshop on Types in Languages Design and Implementation},
	title = {Lightweight Linear Types in {S}ystem {F}},
	year = {2010}}

@inproceedings{necula1997proof,
	author = {George C. Necula},
	booktitle = {Proceedings of the {ACM} {SIGPLAN} Symposium on Principles of Programming Languages},
	title = {Proof-carrying code},
	year = {1997}}

@article{DBLP:journals/corr/abs-1908-04507,
	author = {Huashan Chen and Marcus Pendleton and Laurent Njilla and Shouhuai Xu},
	journal = {CoRR},
	title = {A Survey on Ethereum Systems Security: Vulnerabilities, Attacks and Defenses},
	volume = {abs/1908.04507},
	year = {2019}}

@inproceedings{eth_vulns,
	author = {Nicola Atzei and Massimo Bartoletti and Tiziana Cimoli},
	booktitle = {{POST}},
	pages = {164--186},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Survey of Attacks on Ethereum Smart Contracts (SoK)},
	volume = {10204},
	year = {2017}}

@techreport{capability-myths,
	author = {Mark S. Miller and Ka-Ping Yee and Jonathan Shapiro},
	title = {Capability Myths Demolished},
	year = {2003}}

@article{Hardy94theconfused,
	author = {Norman Hardy},
	journal = {ACM SIGOPS Operating Systems Review},
	pages = {36--38},
	title = {The Confused Deputy (or why capabilities might have been invented)},
	volume = {22},
	year = {1994}}

@article{DBLP:journals/pacmpl/Swasey0D17,
	author = {David Swasey and Deepak Garg and Derek Dreyer},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/journals/pacmpl/Swasey0D17},
	doi = {10.1145/3133913},
	journal = {{PACMPL}},
	number = {{OOPSLA}},
	pages = {89:1--89:26},
	timestamp = {Tue, 06 Nov 2018 12:51:05 +0100},
	title = {Robust and compositional verification of object capability patterns},
	url = {https://doi.org/10.1145/3133913},
	volume = {1},
	year = {2017},
	bdsk-url-1 = {https://doi.org/10.1145/3133913}}

@inproceedings{DBLP:conf/fm/KasampalisGMSZF19,
	author = {Theodoros Kasampalis and Dwight Guth and Brandon M. Moore and Traian{-}Florin Serbanuta and Yi Zhang and Daniele Filaretti and Virgil Nicolae Serbanuta and Ralph Johnson and Grigore Rosu},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/conf/fm/KasampalisGMSZF19},
	booktitle = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019, Porto, Portugal, October 7-11, 2019, Proceedings},
	pages = {593--610},
	timestamp = {Mon, 23 Sep 2019 13:52:37 +0200},
	title = {{IELE:} {A} Rigorously Designed Language and Tool Ecosystem for the Blockchain},
	year = {2019}}

@article{DBLP:journals/corr/abs-1904-06534,
	archiveprefix = {arXiv},
	author = {Franklin Schrans and Daniel Hails and Alexander Harkness and Sophia Drossopoulou and Susan Eisenbach},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/journals/corr/abs-1904-06534},
	eprint = {1904.06534},
	journal = {CoRR},
	timestamp = {Thu, 25 Apr 2019 13:55:01 +0200},
	title = {Flint for Safer Smart Contracts},
	url = {http://arxiv.org/abs/1904.06534},
	volume = {abs/1904.06534},
	year = {2019},
	bdsk-url-1 = {http://arxiv.org/abs/1904.06534}}

@inproceedings{DBLP:conf/icse/Coblenz17,
	author = {Michael J. Coblenz},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/conf/icse/Coblenz17},
	booktitle = {Proceedings of the 39th International Conference on Software Engineering, {ICSE} 2017, Buenos Aires, Argentina, May 20-28, 2017 - Companion Volume},
	doi = {10.1109/ICSE-C.2017.150},
	pages = {97--99},
	timestamp = {Wed, 16 Oct 2019 14:14:49 +0200},
	title = {Obsidian: a safer blockchain programming language},
	url = {https://doi.org/10.1109/ICSE-C.2017.150},
	year = {2017},
	bdsk-url-1 = {https://doi.org/10.1109/ICSE-C.2017.150}}

@article{DBLP:journals/corr/abs-1909-03523,
	archiveprefix = {arXiv},
	author = {Michael J. Coblenz and Reed Oei and Tyler Etzel and Paulette Koronkevich and Miles Baker and Yannick Bloem and Brad A. Myers and Joshua Sunshine and Jonathan Aldrich},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/journals/corr/abs-1909-03523},
	eprint = {1909.03523},
	journal = {CoRR},
	timestamp = {Tue, 17 Sep 2019 11:23:44 +0200},
	title = {Obsidian: Typestate and Assets for Safer Blockchain Programming},
	url = {http://arxiv.org/abs/1909.03523},
	volume = {abs/1909.03523},
	year = {2019},
	bdsk-url-1 = {http://arxiv.org/abs/1909.03523}}

@misc{das2019resourceaware,
	archiveprefix = {arXiv},
	author = {Ankush Das and Stephanie Balzer and Jan Hoffmann and Frank Pfenning},
	eprint = {1902.06056},
	primaryclass = {cs.PL},
	title = {Resource-Aware Session Types for Digital Contracts},
	year = {2019}}

@misc{hyperledger,
	author = {The Linux Foundation},
	howpublished = {\url{https://www.hyperledger.org/projects/fabric}},
	title = {Hyperledger Fabric},
	year = {2018}}

@inproceedings{DBLP:conf/pldi/GrossmanMJHWC02,
	author = {Dan Grossman and J. Gregory Morrisett and Trevor Jim and Michael W. Hicks and Yanling Wang and James Cheney},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/conf/pldi/GrossmanMJHWC02},
	booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002},
	doi = {10.1145/512529.512563},
	pages = {282--293},
	timestamp = {Tue, 06 Nov 2018 16:59:30 +0100},
	title = {Region-Based Memory Management in Cyclone},
	url = {https://doi.org/10.1145/512529.512563},
	year = {2002},
	bdsk-url-1 = {https://doi.org/10.1145/512529.512563}}

@inproceedings{DBLP:conf/popl/TovP11,
	author = {Jesse A. Tov and Riccardo Pucella},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/conf/popl/TovP11},
	booktitle = {Proceedings of the 38th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2011, Austin, TX, USA, January 26-28, 2011},
	doi = {10.1145/1926385.1926436},
	pages = {447--458},
	timestamp = {Tue, 06 Nov 2018 11:07:43 +0100},
	title = {Practical affine types},
	url = {https://doi.org/10.1145/1926385.1926436},
	year = {2011},
	bdsk-url-1 = {https://doi.org/10.1145/1926385.1926436}}

@inproceedings{DBLP:conf/agere/ClebschDBM15,
	author = {Sylvan Clebsch and Sophia Drossopoulou and Sebastian Blessing and Andy McNeil},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/bib/conf/agere/ClebschDBM15},
	booktitle = {Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015},
	doi = {10.1145/2824815.2824816},
	pages = {1--12},
	timestamp = {Sun, 02 Jun 2019 21:20:00 +0200},
	title = {Deny capabilities for safe, fast actors},
	url = {https://doi.org/10.1145/2824815.2824816},
	year = {2015},
	bdsk-url-1 = {https://doi.org/10.1145/2824815.2824816}}

@inproceedings{Smetsers:1993:GSD:647364.725667,
	acmid = {725667},
	address = {Berlin, Heidelberg},
	author = {Smetsers, Sjaak and Barendsen, Erik and Eekelen, Marko C. J. D. van and Plasmeijer, Marinus J.},
	booktitle = {Proceedings of the International Workshop on Graph Transformations in Computer Science},
	isbn = {3-540-57787-4},
	numpages = {22},
	pages = {358--379},
	publisher = {Springer-Verlag},
	title = {Guaranteeing Safe Destructive Updates Through a Type System with Uniqueness Information for Graphs},
	url = {http://dl.acm.org/citation.cfm?id=647364.725667},
	year = {1994},
	bdsk-url-1 = {http://dl.acm.org/citation.cfm?id=647364.725667}}

@book{Ethan:2017:BWS:3165061,
	address = {USA},
	author = {Ethan, Maynard},
	isbn = {1548488062, 9781548488062},
	publisher = {CreateSpace Independent Publishing Platform},
	title = {Bitcoin Wallet Security: The Essential Guide to Bitcoin Wallet Security},
	year = {2017}}

@article{rust,
	acmid = {2663188},
	address = {New York, NY, USA},
	author = {Matsakis, Nicholas D. and Klock,II, Felix S.},
	doi = {10.1145/2692956.2663188},
	issn = {1094-3641},
	issue_date = {December 2014},
	journal = {Ada Lett.},
	keywords = {affine type systems, memory management, rust, systems programming},
	month = oct,
	number = {3},
	numpages = {2},
	pages = {103--104},
	publisher = {ACM},
	title = {{The Rust Language},
	NOurl = {http://doi.acm.org/10.1145/2692956.2663188}},
	volume = {34},
	year = {2014},
	bdsk-url-1 = {http://doi.acm.org/10.1145/2692956.2663188},
	bdsk-url-2 = {https://doi.org/10.1145/2692956.2663188}}

@book{c++,
	author = {Stroustrup, Bjarne},
	edition = {4th},
	isbn = {0321563840, 9780321563842},
	publisher = {Addison-Wesley Professional},
	title = {The C++ Programming Language},
	year = {2013}}

@inproceedings{BCD+11,
	author = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovi\'c and Tim King and Andrew Reynolds and Cesare Tinelli},
	booktitle = {Proceedings of the $23^{rd}$ International Conference on Computer Aided Verification (CAV '11)},
	editor = {Ganesh Gopalakrishnan and Shaz Qadeer},
	month = jul,
	note = {{Snowbird, Utah}},
	pages = {171--177},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {{CVC4}},
	volume = 6806,
	year = 2011}

@inproceedings{z3,
	author = {Leonardo Mendon{\c{c}}a de Moura and Nikolaj Bj{\o}rner},
	booktitle = {{TACAS}},
	pages = {337--340},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {{Z3:} An Efficient {SMT} Solver},
	volume = {4963},
	year = {2008}}

@misc{hacks-on-smart-contracts,
	author = {{Morisander}},
	title = {{The Biggest Smart Contract Hacks in History Or How to Endanger up to US \$2.2 Billion}},
	howpublished = {\url{https://medium.com/solidified/the-biggest-smart-contract-hacks-in-history-or-how-to-endanger-up-to-us-2-2-billion-d5a72961d15d}},
	year = {2018}}

@misc{hacks-on-compound,
	author = {MacKenzie Sigalos},
	title = {{Bug Puts \$162 Million up for Grabs, Says Founder of DeFi Platform Compound}},
	howpublished = {\url{https://www.cnbc.com/2021/10/03/162-million-up-for-grabs-after-bug-in-defi-protocol-compound-.html}},
	year = {2021}}

@misc{StateConstraintsPatent,
   author = {Nikolai Tillmann and Wolfgang Grieskamp and Wolfram Schulte},
   title = {Efficient checking of state-dependent constraints},
   year = {U.S. Patent 20050198621A1, 2004}
}

@misc{MVP_ARTIFACT,
	author = {{Meng Xu}},
	title = {{Artifact for Paper ``Fast and Reliable Formal Verification of Smart Contracts with the Move Prover''}},

	url = {https://github.com/meng-xu-cs/mvp-artifact},
	bdsk-url-1 = {https://github.com/meng-xu-cs/mvp-artifact},
	year = 2020,
}