@article{DBLP:journals/corr/abs-2021,
    title={Verification of the Incremental Merkle Tree Algorithm with Dafny}, 
    author={Franck Cassez},
    year={2021},
    eprint={2105.06009},
    archivePrefix={arXiv},
    primaryClass={cs.LO},
    abstract={
    The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.
    },
  journal   = {CoRR},
  volume    = {abs/2105.06009},
  url       = {https://arxiv.org/abs/2105.06009}
}

{"_id":"Ppbn2vcgoEYhHWyAp","bibbaseid":"cassez-verificationoftheincrementalmerkletreealgorithmwithdafny-2021","author_short":["Cassez, F."],"bibdata":{"bibtype":"article","type":"article","title":"Verification of the Incremental Merkle Tree Algorithm with Dafny","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]}],"year":"2021","eprint":"2105.06009","archiveprefix":"arXiv","primaryclass":"cs.LO","abstract":"The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm. ","journal":"CoRR","volume":"abs/2105.06009","url":"https://arxiv.org/abs/2105.06009","bibtex":"@article{DBLP:journals/corr/abs-2021,\n title={Verification of the Incremental Merkle Tree Algorithm with Dafny}, \n author={Franck Cassez},\n year={2021},\n eprint={2105.06009},\n archivePrefix={arXiv},\n primaryClass={cs.LO},\n abstract={\n The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.\n },\n journal = {CoRR},\n volume = {abs/2105.06009},\n url = {https://arxiv.org/abs/2105.06009}\n}\n \n","author_short":["Cassez, F."],"key":"DBLP:journals/corr/abs-2021","id":"DBLP:journals/corr/abs-2021","bibbaseid":"cassez-verificationoftheincrementalmerkletreealgorithmwithdafny-2021","role":"author","urls":{"Paper":"https://arxiv.org/abs/2105.06009"},"metadata":{"authorlinks":{}},"downloads":13,"html":""},"bibtype":"article","biburl":"https://franck44.github.io/publications/franck-pubs.bib","dataSources":["8742EsvjQfyP2fYBW"],"keywords":[],"search_terms":["verification","incremental","merkle","tree","algorithm","dafny","cassez"],"title":"Verification of the Incremental Merkle Tree Algorithm with Dafny","year":2021,"downloads":13}