main.bib

@string{ SV = {Springer} }
@string{ LNCS = {LNCS} }
@string{ ACM = {ACM} }
@string{ IEEE = {IEEE} }
@string{ SMT = {SMT} }

@inproceedings{Bhargavan2016,
 author = {Bhargavan, Karthikeyan and Delignat-Lavaud, Antoine and Fournet, C{\'e}dric and Gollamudi, Anitha and Gonthier, Georges and Kobeissi, Nadim and Kulatova, Natalia and Rastogi, Aseem and Sibut-Pinote, Thomas and Swamy, Nikhil and Zanella-B{\'e}guelin, Santiago},
 title = {Formal Verification of Smart Contracts: Short Paper},
 booktitle = {Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security},
 series = {PLAS '16},
 year = {2016},
 pages = {91--96}
} 

@inproceedings{Luu2016,
 author = {Luu, Loi and Chu, Duc-Hiep and Olickel, Hrishi and Saxena, Prateek and Hobor, Aquinas},
 title = {Making Smart Contracts Smarter},
 booktitle = {Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security},
 series = {CCS '16},
 year = {2016},
 pages = {254--269}
}

@inproceedings{Hirai2017,
  author    = {Yoichi Hirai},
  title     = {Defining the Ethereum Virtual Machine for Interactive Theorem Provers},
  booktitle = {Financial Cryptography and Data Security - {FC} 2017 International
               Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April
               7, 2017, Revised Selected Papers},
  pages     = {520--535},
  year      = {2017}
}

@online{SolidityDocs,
  author = {Ethereum},
  title = {Solidity Documentation v0.4.21},
  year = 2018,
  url = {solidity.readthedocs.io},
  urldate = {2018-04-07}
}

@online{WhitePaper,
  author = {Vitalik Buterin},
  title = {A Next-Generation Smart Contract and Decentralized Application Platform},
  year = 2014,
  url = {github.com/ethereum/wiki/wiki/White-Paper},
  urldate = {2018-04-07}
}

@online{YellowPaper,
  author = {Gavin Wood},
  title = {Ethereum: A Secure Decentralised Generalised Transaction Ledger},
  year = 2018,
  url = {ethereum.github.io/yellowpaper/paper.pdf},
  urldate = {2018-04-07}
}

@InProceedings{Biere99,
author="Biere, Armin
and Cimatti, Alessandro
and Clarke, Edmund
and Zhu, Yunshan",
title="Symbolic Model Checking without {BDDs}",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="1999",
publisher="Springer",
pages="193--207"
}

@InProceedings{Donaldson11,
author="Donaldson, Alastair F.
and Haller, Leopold
and Kroening, Daniel
and R{\"u}mmer, Philipp",
title="Software Verification Using k-Induction",
booktitle="Static Analysis",
year="2011",
publisher="Springer",
pages="351--368"
}

@InProceedings{Komuravelli13,
author="Komuravelli, Anvesh
and Gurfinkel, Arie
and Chaki, Sagar
and Clarke, Edmund M.",
title="Automatic Abstraction in {SMT}-Based Unbounded Software Model Checking",
booktitle="Computer Aided Verification",
year="2013",
publisher="Springer",
pages="846--862"
}

@InProceedings{Beyer11,
author="Beyer, Dirk
and Keremoglu, M. Erkan",
title="CPAchecker: A Tool for Configurable Software Verification",
booktitle="Computer Aided Verification",
year="2011",
publisher="Springer",
pages="184--190"
}

@InProceedings{Kroening14,
author="Kroening, Daniel
and Tautschnig, Michael",
title="{CBMC} -- C Bounded Model Checker",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2014",
publisher="Springer",
pages="389--391"
}

@InProceedings{Alt17,
author="Alt, Leonardo
and Asadi, Sepideh
and Chockler, Hana
and Even Mendoza, Karine
and Fedyukovich, Grigory
and Hyv{\"a}rinen, Antti E. J.
and Sharygina, Natasha",
title="{HiFrog}: {SMT}-based Function Summarization for Software Verification",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2017",
publisher="Springer",
pages="207--213"
}

@article{Grossman2017,
 author = {Grossman, Shelly and Abraham, Ittai and Golan-Gueta, Guy and Michalevsky, Yan and Rinetzky, Noam and Sagiv, Mooly and Zohar, Yoni},
 title = {Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts},
 journal = {Proc. ACM Program. Lang.},
 volume = {2},
 number = {POPL},
 year = {2017},
 pages = {48:1--48:28},
 publisher = {ACM}
} 

@online{Mythril,
  author = {ConsenSys},
  title = {Mythril},
  year = 2018,
  url = {github.com/ConsenSys/mythril},
  urldate = {2018-04-07}
}

@online{Why3,
  author = {Why3},
  title = {Why3},
  year = 2018,
  url = {why3.lri.fr},
  urldate = {2018-04-07}
}

@online{SafeMath,
  author = {OpenZeppelin},
  title = "{SafeMath}",
  year = 2018,
  url = {github.com/OpenZeppelin/zeppelin-solidity/blob/master/contracts/math/SafeMath.sol},
  urldate = {2018-04-09}
}

@InProceedings{Z3,
author="de Moura, Leonardo
and Bj{\o}rner, Nikolaj",
title="Z3: An Efficient {SMT} Solver",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2008",
publisher="Springer",
pages="337--340"
}

@InProceedings{CVC4,
author="Barrett, Clark
and Conway, Christopher L.
and Deters, Morgan
and Hadarean, Liana
and Jovanovi{\'{c}}, Dejan
and King, Tim
and Reynolds, Andrew
and Tinelli, Cesare",
title="{CVC4}",
booktitle="Computer Aided Verification",
year="2011",
publisher="Springer",
pages="171--177"
}

@online{SMTLIB,
  author = {SMT-LIB},
  title = "{SMT-LIB}",
  year = 2018,
  url = {smtlib.cs.uiowa.edu},
  urldate = {2018-04-09}
}

@article{Grossman,
 author = {Grossman, Shelly and Abraham, Ittai and Golan-Gueta, Guy and Michalevsky, Yan and Rinetzky, Noam and Sagiv, Mooly and Zohar, Yoni},
 title = {Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts},
 journal = {Proc. ACM Program. Lang.},
 volume = {2},
 number = {POPL},
 year = {2017},
 pages = {48:1--48:28},
 publisher = {ACM},
 address = {New York}
} 

@article{ZEUS,
 author = {
 Kalra, Sukrit and
 Goel, Seep and
 Dhawan, Mohan and
 Sharma, Subodh},
 title = "{ZEUS}: Analyzing Safety of Smart Contracts",
 year = {2018},
 booktitle = {To appear in Proceedings of the {NDSS}},
}

@article{NKSSH18,
  author    = {Ivica Nikolic and
               Aashish Kolluri and
               Ilya Sergey and
               Prateek Saxena and
               Aquinas Hobor},
  title     = {Finding The Greedy, Prodigal, and Suicidal Contracts at Scale},
  journal   = {CoRR},
  volume    = {abs/1802.06038},
  year      = {2018},
  url       = {http://arxiv.org/abs/1802.06038},
  archivePrefix = {arXiv},
  eprint    = {1802.06038},
  timestamp = {Thu, 01 Mar 2018 19:20:48 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1802-06038},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}