| dc.contributor.author | Jehl, Leander | |
| dc.date.accessioned | 2023-02-28T15:11:19Z | |
| dc.date.available | 2023-02-28T15:11:19Z | |
| dc.date.created | 2021-12-14T10:59:16Z | |
| dc.date.issued | 2021 | |
| dc.identifier.citation | Jehl, L. (2021, June). Formal verification of hotstuff. In Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings (pp. 197-204). Cham: Springer International Publishing. | en_US |
| dc.identifier.isbn | 978-3-030-78089-0 | |
| dc.identifier.uri | https://hdl.handle.net/11250/3054769 | |
| dc.description.abstract | HotStuff is a recent algorithm for repeated distributed consensus used in permissioned blockchains. We present a simplified version of the HotStuff algorithm and verify its safety using both Ivy and the TLA Proof Systems tools.
We show that HotStuff deviates from the traditional view-instance model used in other consensus algorithms and instead follows a novel tree model to solve this fundamental problem. We argue that the tree model results in more complex verification tasks than the traditional view-instance model. Our verification efforts provide initial evidence towards this claim. | en_US |
| dc.language.iso | eng | en_US |
| dc.publisher | Springer | en_US |
| dc.relation.ispartof | Formal Techniques for Distributed Objects, Components, and Systems | |
| dc.title | Formal Verification of HotStuff | en_US |
| dc.type | Chapter | en_US |
| dc.description.version | acceptedVersion | en_US |
| dc.rights.holder | The owners/authors | en_US |
| dc.subject.nsi | VDP::Teknologi: 500 | en_US |
| dc.identifier.doi | 10.1007/978-3-030-78089-0_13 | |
| dc.identifier.cristin | 1968160 | |
| dc.relation.project | Norges forskningsråd: 274451 | en_US |
| cristin.ispublished | true | |
| cristin.fulltext | postprint | |
| cristin.qualitycode | 1 | |
