@article{DBLP:journals/corr/abs-2208-02920,
  author    = {Franck Cassez and
               Joanne Fuller and
               Horacio Mijail Anton Quiles},
  title     = {Deductive Verification of Smart Contracts with Dafny},
  journal   = {CoRR},
  volume    = {abs/2208.02920},
  year      = {2022},
  url       = {https://doi.org/10.48550/arXiv.2208.02920},
  doi       = {10.48550/arXiv.2208.02920},
  eprinttype = {arXiv},
  eprint    = {2208.02920},
  timestamp = {Wed, 10 Aug 2022 14:49:54 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2208-02920.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  abstract = {We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.}
}

{"_id":"invKmHrdZYndsNq94","bibbaseid":"cassez-fuller-quiles-deductiveverificationofsmartcontractswithdafny-2022","author_short":["Cassez, F.","Fuller, J.","Quiles, H. M. A."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Joanne"],"propositions":[],"lastnames":["Fuller"],"suffixes":[]},{"firstnames":["Horacio","Mijail","Anton"],"propositions":[],"lastnames":["Quiles"],"suffixes":[]}],"title":"Deductive Verification of Smart Contracts with Dafny","journal":"CoRR","volume":"abs/2208.02920","year":"2022","url":"https://doi.org/10.48550/arXiv.2208.02920","doi":"10.48550/arXiv.2208.02920","eprinttype":"arXiv","eprint":"2208.02920","timestamp":"Wed, 10 Aug 2022 14:49:54 +0200","biburl":"https://dblp.org/rec/journals/corr/abs-2208-02920.bib","bibsource":"dblp computer science bibliography, https://dblp.org","abstract":"We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.","bibtex":"@article{DBLP:journals/corr/abs-2208-02920,\n author = {Franck Cassez and\n Joanne Fuller and\n Horacio Mijail Anton Quiles},\n title = {Deductive Verification of Smart Contracts with Dafny},\n journal = {CoRR},\n volume = {abs/2208.02920},\n year = {2022},\n url = {https://doi.org/10.48550/arXiv.2208.02920},\n doi = {10.48550/arXiv.2208.02920},\n eprinttype = {arXiv},\n eprint = {2208.02920},\n timestamp = {Wed, 10 Aug 2022 14:49:54 +0200},\n biburl = {https://dblp.org/rec/journals/corr/abs-2208-02920.bib},\n bibsource = {dblp computer science bibliography, https://dblp.org},\n abstract = {We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language DAFNY. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from DAFNY to EVM bytecode, the results we obtain on the DAFNY code can reasonably be assumed to hold on Solidity code: the translation of the DAFNY code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.}\n}\n\n\n","author_short":["Cassez, F.","Fuller, J.","Quiles, H. M. A."],"key":"DBLP:journals/corr/abs-2208-02920","id":"DBLP:journals/corr/abs-2208-02920","bibbaseid":"cassez-fuller-quiles-deductiveverificationofsmartcontractswithdafny-2022","role":"author","urls":{"Paper":"https://doi.org/10.48550/arXiv.2208.02920"},"metadata":{"authorlinks":{}},"downloads":5,"html":""},"bibtype":"article","biburl":"https://franck44.github.io/publications/franck-pubs.bib","dataSources":["8742EsvjQfyP2fYBW"],"keywords":[],"search_terms":["deductive","verification","smart","contracts","dafny","cassez","fuller","quiles"],"title":"Deductive Verification of Smart Contracts with Dafny","year":2022,"downloads":6}