{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:44:14Z","timestamp":1743065054209,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030217587"},{"type":"electronic","value":"9783030217594"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-21759-4_12","type":"book-chapter","created":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T23:30:20Z","timestamp":1559518220000},"page":"204-223","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Verified Blockchain Architectures: A Case Study on Interactive Architecture Verification"],"prefix":"10.1007","author":[{"given":"Diego","family":"Marmsoler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,29]]},"reference":[{"key":"12_CR1","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-662-53357-4_10","volume-title":"Financial Cryptography and Data Security","author":"I Bentov","year":"2016","unstructured":"Bentov, I., Gabizon, A., Mizrahi, A.: Cryptocurrencies without proof of work. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 142\u2013157. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53357-4_10"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Azaria, A., Ekblaw, A., Vieira, T., Lippman, A.: MedRec: using blockchain for medical data access and permission management. In: International Conference on Open and Big Data (OBD), pp. 25\u201330. IEEE (2016)","DOI":"10.1109\/OBD.2016.11"},{"key":"12_CR4","unstructured":"Chavez-Dreyfuss, G.: Sweden tests blockchain technology for land registry. http:\/\/web.archive.org\/web\/20161024065806\/www.reuters.com\/article\/us-sweden-blockchain-idUSKCN0Z22KV"},{"issue":"1","key":"12_CR5","first-page":"4","volume":"9","author":"J Mendling","year":"2018","unstructured":"Mendling, J., et al.: Blockchains for business process management-challenges and opportunities. ACM Trans. Manag. Inf. Syst. (TMIS) 9(1), 4 (2018)","journal-title":"ACM Trans. Manag. Inf. Syst. (TMIS)"},{"key":"12_CR6","unstructured":"Yurcan, B.: How blockchain fits into the future of digital identity. http:\/\/web.archive.org\/web\/20170119054131\/https:\/\/www.americanbanker.com\/news\/how-blockchain-fits-into-the-future-of-digital-identity"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-46750-4_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"D Marmsoler","year":"2016","unstructured":"Marmsoler, D., Gleirscher, M.: Specifying properties of dynamic architectures using configuration traces. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 235\u2013254. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_14"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-319-89363-1_9","volume-title":"Fundamental Approaches to Software Engineering","author":"D Marmsoler","year":"2018","unstructured":"Marmsoler, D.: Hierarchical specification and verification of architectural design patterns. In: Russo, A., Sch\u00fcrr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 149\u2013168. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89363-1_9"},{"key":"12_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"12_CR10","unstructured":"The Bitcoin Community: The bitcoin wiki. http:\/\/web.archive.org\/web\/20181106124036\/https:\/\/en.bitcoin.it\/wiki\/Confirmation"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-030-02146-7_14","volume-title":"Formal Aspects of Component Software","author":"D Marmsoler","year":"2018","unstructured":"Marmsoler, D., Gidey, H.K.: FACTum studio: a tool for the axiomatic specification and verification of architectural design patterns. In: Bae, K., \u00d6lveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 279\u2013287. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02146-7_14"},{"issue":"2","key":"12_CR12","first-page":"187","volume":"26","author":"D Marmsoler","year":"2016","unstructured":"Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architectures. Sci. Ann. Comput. Sci. 26(2), 187\u2013248 (2016)","journal-title":"Sci. Ann. Comput. Sci."},{"issue":"10","key":"12_CR13","doi-asserted-by":"publisher","first-page":"1758","DOI":"10.1093\/comjnl\/bxq005","volume":"53","author":"M Broy","year":"2010","unstructured":"Broy, M.: A logical basis for component-oriented software and systems engineering. Comput. J. 53(10), 1758\u20131782 (2010)","journal-title":"Comput. J."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-030-02450-5_15","volume-title":"Formal Methods and Software Engineering","author":"D Marmsoler","year":"2018","unstructured":"Marmsoler, D.: A framework for interactive verification of architectural design patterns in Isabelle\/HOL. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_15"},{"key":"12_CR15","first-page":"675","volume-title":"Formal Models and Semantics","author":"Martin WIRSING","year":"1990","unstructured":"Wirsing, M.: Algebraic specification. In: van Leeuwen, J., (ed.): Handbook of Theoretical Computer Science, vol. B, pp. 675\u2013788. MIT Press, Cambridge, MA, USA (1990)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Marmsoler, D.: Axiomatic specification and interactive verification of architectural design patterns in FACTum. Dissertation, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen (2019)","DOI":"10.1007\/s00165-019-00488-x"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-67729-3_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2017\u201314th International Colloquium, Hanoi, Vietnam, 23\u201327 October 2017","author":"D Marmsoler","year":"2017","unstructured":"Marmsoler, D.: Towards a calculus for dynamic architectures. In: Hung, D.V., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 79\u201399. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-67729-3_6"},{"key":"12_CR18","unstructured":"Marmsoler, D.: A theory of architectural design patterns. Archive of Formal Proofs, March 2018. Formal proof development. http:\/\/isa-afp.org\/entries\/Architectural_Design_Patterns.html"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48184-2_32","volume-title":"Advances in Cryptology \u2014 CRYPTO 1987","author":"RC Merkle","year":"1988","unstructured":"Merkle, R.C.: A digital signature based on a conventional encryption function. In: Pomerance, C. (ed.) CRYPTO 1987. LNCS, vol. 293, pp. 369\u2013378. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-48184-2_32"},{"issue":"9","key":"12_CR20","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2701411","volume":"58","author":"A Zohar","year":"2015","unstructured":"Zohar, A.: Bitcoin: under the hood. Commun. ACM 58(9), 104\u2013113 (2015)","journal-title":"Commun. ACM"},{"key":"12_CR21","unstructured":"Hirai, Y.: Ethereum virtual machine for Coq (v0. 0.2). Published online on, 5 March 2017"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91\u201396. ACM (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Brousmiche, K.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1\u20135, February 2018","DOI":"10.1109\/NTMS.2018.8328737"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-89722-6_11","volume-title":"Principles of Security and Trust","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Tool demonstration: FSolidM for designing secure ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 270\u2013277. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_11"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 66\u201377. ACM (2018)","DOI":"10.1145\/3167084"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"P\u00eerlea, G., Sergey, I.: Mechanising blockchain consensus. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 78\u201390. ACM (2018)","DOI":"10.1145\/3167086"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Zufferey, D.: PSYNC: a partially synchronous language for fault-tolerant distributed algorithms. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 400\u2013415. ACM, New York (2016)","DOI":"10.1145\/2837614.2837650"},{"key":"12_CR29","unstructured":"Jaskelioff, M., Merz, S.: Proving the correctness of disk Paxos. The Archive of Formal Proofs (2005). http:\/\/afp.sf.net\/entries\/DiskPaxos.shtml"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for formally verifying distributed system implementations. In: Proceedings of the 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Portland, OR (2015)","DOI":"10.1145\/2737924.2737958"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the raft consensus protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 154\u2013165. ACM (2016)","DOI":"10.1145\/2854065.2854081"},{"issue":"POPL","key":"12_CR32","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3158116","volume":"2","author":"I Sergey","year":"2017","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 28 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-63688-7_12","volume-title":"Advances in Cryptology \u2013 CRYPTO 2017","author":"A Kiayias","year":"2017","unstructured":"Kiayias, A., Russell, A., David, B., Oliynykov, R.: Ouroboros: a provably secure proof-of-stake blockchain protocol. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10401, pp. 357\u2013388. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63688-7_12"},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-662-46803-6_10","volume-title":"Advances in Cryptology - EUROCRYPT 2015","author":"J Garay","year":"2015","unstructured":"Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol: analysis and applications. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9057, pp. 281\u2013310. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46803-6_10"},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-63688-7_10","volume-title":"Advances in Cryptology \u2013 CRYPTO 2017","author":"J Garay","year":"2017","unstructured":"Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol with chains of variable difficulty. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10401, pp. 291\u2013323. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63688-7_10"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-56614-6_22","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2017","author":"R Pass","year":"2017","unstructured":"Pass, R., Seeman, L., Shelat, A.: Analysis of the blockchain protocol in asynchronous networks. In: Coron, J.-S., Nielsen, J.B. (eds.) EUROCRYPT 2017. LNCS, vol. 10211, pp. 643\u2013673. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-56614-6_22"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-21759-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T00:04:09Z","timestamp":1685750649000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-21759-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030217587","9783030217594"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-21759-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Copenhagen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 June 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"39","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2019\/forte","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}