%0 Conference Proceedings
%T Towards Verified Blockchain Architectures: A Case Study on Interactive Architecture Verification
%+ Technische Universität Munchen - Technical University Munich - Université Technique de Munich (TUM)
%A Marmsoler, Diego
%Z Part 1: Full Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-11535
%P 204-223
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_12
%K Blockchain
%K Interactive theorem proving
%K Dynamic architectures
%K Factum
%K Isabelle
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X With the emergence of cryptocurrencies, Blockchain architectures have become more and more important. In such architectures, components maintain and exchange a list of records in a way which makes the entries persistent, i.e., resistant to modifications. Thereby, the architecture is dynamic in the sense that components may join or leave the network and connections between them may change over time. The dynamic nature of Blockchain architectures makes their verification a challenge, since it involves reasoning about potentially unbounded number of components. To this end, we developed FACTum, an approach for the specification and interactive verification of dynamic architectures based on the interactive theorem prover Isabelle. In this paper we report on the outcome of applying the approach to formally specify a version of Blockchain architectures and verify that the list entries of such architectures are indeed persistent.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313742/document
%2 https://inria.hal.science/hal-02313742/file/478668_1_En_12_Chapter.pdf
%L hal-02313742
%U https://inria.hal.science/hal-02313742
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535