{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:31:52Z","timestamp":1742992312889,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031671135"},{"type":"electronic","value":"9783031671142"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-67114-2_8","type":"book-chapter","created":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:42:47Z","timestamp":1725507767000},"page":"172-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstracting and\u00a0Verifying Decentralised Systems in\u00a0CSP"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7557-3901","authenticated-orcid":false,"given":"A. W.","family":"Roscoe","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-0910","authenticated-orcid":false,"given":"Pedro","family":"Antonino","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4884-6684","authenticated-orcid":false,"given":"Jonathan","family":"Lawrence","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,1]]},"reference":[{"key":"8_CR1","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., Wallach, D., Brenner, M., Rohloff, K. (eds.) Financial Cryptography and Data Security, pp. 142\u2013157. Springer, Heidelberg (2016)"},{"doi-asserted-by":"publisher","unstructured":"Brookes, S.D., Roscoe, A.W.: CSP: a practical process algebra. In: Theories of Programming: The Life and Works of Tony Hoare, 1 edn., pp. 187\u2013222. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3477355.3477365","key":"8_CR2","DOI":"10.1145\/3477355.3477365"},{"unstructured":"Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on BFT consensus. CoRR arXiv:1807.04938 (2018)","key":"8_CR3"},{"unstructured":"Buterin, V.: Ethereum: a next-generation smart contract and decentralized application platform (2014). https:\/\/ethereum.org\/whitepaper\/","key":"8_CR4"},{"doi-asserted-by":"publisher","unstructured":"Camenisch, J., Drijvers, M., Hanke, T., Pignolet, Y.A., Shoup, V., Williams, D.: Internet computer consensus. In: Proceedings of the 2022 ACM Symposium on Principles of Distributed Computing, pp. 81\u201391. PODC 2022. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3519270.3538430","key":"8_CR5","DOI":"10.1145\/3519270.3538430"},{"issue":"6\u201310","key":"8_CR6","first-page":"71","volume":"2","author":"M Crosby","year":"2016","unstructured":"Crosby, M., Pattanayak, P., Verma, S., Kalyanaraman, V., et al.: Blockchain technology: beyond bitcoin. Appl. Innov. 2(6\u201310), 71 (2016)","journal-title":"Appl. Innov."},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"76","DOI":"10.3905\/jpm.2008.709984","volume":"34","author":"K Dowd","year":"2008","unstructured":"Dowd, K., Cotter, J., Humphrey, C., Woods, M.: How unlucky is 25-sigma? J. Portfolio Manage. 34, 76\u201380 (2008). https:\/\/doi.org\/10.3905\/jpm.2008.709984","journal-title":"J. Portfolio Manage."},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM (JACM) 35(2), 288\u2013323 (1988)","journal-title":"J. ACM (JACM)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"issue":"5","key":"8_CR10","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s10009-019-00516-4","volume":"21","author":"T Gibson-Robinson","year":"2019","unstructured":"Gibson-Robinson, T., Lowe, G.: Symmetry reduction in CSP model checking. Int. J. Softw. Tools Technol. Transfer 21(5), 567\u2013605 (2019)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"doi-asserted-by":"publisher","unstructured":"Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: scaling byzantine agreements for cryptocurrencies. In: Proceedings of the 26th Symposium on Operating Systems Principles, pp. 51\u201368. SOSP 2017. Association for Computing Machinery, New York (2017).https:\/\/doi.org\/10.1145\/3132747.3132757","key":"8_CR11","DOI":"10.1145\/3132747.3132757"},{"doi-asserted-by":"crossref","unstructured":"Goldsmith, M., Moffat, N., Roscoe, B., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model-checking. In: FME, pp. 600\u2013616 (2003)","key":"8_CR12","DOI":"10.1007\/978-3-540-45236-2_33"},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-21668-3_26","volume-title":"Computer Aided Verification","author":"C Hawblitzel","year":"2015","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 449\u2013465. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26"},{"doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)","key":"8_CR15","DOI":"10.1007\/978-3-642-82921-5_4"},{"unstructured":"Hopkins, D., Roscoe, A.W.: SVA, a tool for analysing shared-variable programms. In: Proceedings of AVoCS 2007, pp. 177\u2013183 (2007). http:\/\/web.comlab.ox.ac.uk\/oucl\/work\/bill.roscoe\/publications\/119.pdf","key":"8_CR16"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-63688-7_12","volume-title":"Advances in Cryptology - 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.) Advances in Cryptology - CRYPTO 2017, pp. 357\u2013388. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63688-7_12"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-96145-3_5","volume-title":"Computer Aided Verification","author":"B Kragl","year":"2018","unstructured":"Kragl, B., Qadeer, S.: Layered concurrent programs. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 79\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_5"},{"issue":"2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (1998). https:\/\/doi.org\/10.1145\/279227.279229","journal-title":"ACM Trans. Comput. Syst."},{"key":"8_CR20","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, USA (2002)"},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982). https:\/\/doi.org\/10.1145\/357172.357176","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"8_CR22","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994). https:\/\/doi.org\/10.1145\/197320.197383","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1\u20132","key":"8_CR23","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1\u20132), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"unstructured":"Nakamoto, S., et\u00a0al.: Bitcoin: A Peer-to-peer Electronic Cash System (2008)","key":"8_CR24"},{"unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, pp. 305\u2013320. USENIX ATC 2014, USENIX Association, USA (2014)","key":"8_CR25"},{"issue":"2","key":"8_CR26","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228\u2013234 (1980). https:\/\/doi.org\/10.1145\/322186.322188","journal-title":"J. ACM"},{"doi-asserted-by":"publisher","unstructured":"Rabin, M.O.: Randomized byzantine generals. In: 24th Annual Symposium on Foundations of Computer Science (sfcs 1983), pp. 403\u2013409 (1983). https:\/\/doi.org\/10.1109\/SFCS.1983.48","key":"8_CR27","DOI":"10.1109\/SFCS.1983.48"},{"unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)","key":"8_CR28"},{"doi-asserted-by":"publisher","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer (2010). https:\/\/doi.org\/10.1007\/978-1-84882-258-0","key":"8_CR29","DOI":"10.1007\/978-1-84882-258-0"},{"doi-asserted-by":"publisher","unstructured":"Roscoe, A.W., Antonino, P., Lawrence, J.: The consensus machine: formalising consensus in the presence of malign agents. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol. 14080, pp. 136\u2013162. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8_6","key":"8_CR30","DOI":"10.1007\/978-3-031-40436-8_6"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AW Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check $$10^{20}$$ dining philosophers for deadlock. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133\u2013152. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_7"},{"doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check $$10^{\\text{20}}$$ dining philosophers for deadlock. In: TACAS, pp. 133\u2013152 (1995)","key":"8_CR32","DOI":"10.1007\/3-540-60630-0_7"},{"unstructured":"Roscoe, A. W.: Model-checking CSP, chap.\u00a021. Prentice Hall (1994). http:\/\/www.cs.ox.ac.uk\/people\/bill.roscoe\/publications\/50.ps","key":"8_CR33"},{"unstructured":"Swan, M.: Blockchain: Blueprint for a New Economy. O\u2019Reilly Media, Inc. (2015)","key":"8_CR34"},{"doi-asserted-by":"publisher","unstructured":"Szymanski, B.K.: A simple solution to lamport\u2019s concurrent programming problem with linear wait. In: Proceedings of the 2nd International Conference on Supercomputing, pp. 621\u2013626. ICS 1988. Association for Computing Machinery, New York (1988). https:\/\/doi.org\/10.1145\/55364.55425","key":"8_CR35","DOI":"10.1145\/55364.55425"},{"unstructured":"Wood, G.: Ethereum Yellow Paper. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf","key":"8_CR36"},{"doi-asserted-by":"publisher","unstructured":"Yin, M., Malkhi, D., Reiter, M.K., Gueta, G.G., Abraham, I.: HotStuff: BFT consensus with linearity and responsiveness. In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, pp. 347\u2013356. PODC 2019. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3293611.3331591","key":"8_CR37","DOI":"10.1145\/3293611.3331591"}],"container-title":["Lecture Notes in Computer Science","The Application of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67114-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:45:42Z","timestamp":1725507942000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67114-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031671135","9783031671142"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67114-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}