{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T12:20:50Z","timestamp":1756383650335,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031471148"},{"type":"electronic","value":"9783031471155"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-47115-5_11","type":"book-chapter","created":{"date-parts":[[2023,10,30]],"date-time":"2023-10-30T15:04:38Z","timestamp":1698678278000},"page":"184-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["SSCalc: A\u00a0Calculus for\u00a0Solidity Smart Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-7673","authenticated-orcid":false,"given":"Diego","family":"Marmsoler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Billy","family":"Thornton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,31]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 9\u201324. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_2","DOI":"10.1007\/978-3-030-61467-6_2"},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227","volume":"67","author":"M Almakhour","year":"2020","unstructured":"Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervas. Mob. Comput. 67, 101227 (2020). https:\/\/doi.org\/10.1016\/j.pmcj.2020.101227","journal-title":"Pervas. Mob. Comput."},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Apt, K.R., de Boer, F., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, London (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","DOI":"10.1007\/978-1-84882-745-5"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Azaria, A., Ekblaw, A., Vieira, T., Lippman, A.: Medrec: using blockchain for medical data access and permission management. In: 2016 2nd International Conference on Open and Big Data (OBD), pp. 25\u201330 (2016). https:\/\/doi.org\/10.1109\/OBD.2016.11","DOI":"10.1109\/OBD.2016.11"},{"key":"11_CR6","unstructured":"Bahrynovska, T.: History of Ethereum Security Vulnerabilities, Hacks and Their Fixes. https:\/\/applicature.com\/blog\/blockchain-technology\/history-of-ethereum-security-vulnerabilities-hacks-and-their-fixes. Accessed 18 Apr 2023"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Galletta, L., Murgia, M.: A minimal core calculus for solidity contracts. In: P\u00e9rez-Sol\u00e0, C., Navarro-Arribas, G., Biryukov, A., Garcia-Alfaro, J. (eds.) DPM\/CBT -2019. LNCS, vol. 11737, pp. 233\u2013243. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31500-9_15","DOI":"10.1007\/978-3-030-31500-9_15"},{"key":"11_CR8","unstructured":"Batra, G., Olson, R., Pathak, S., Santhanam, N., Soundararajan, H.: Blockchain 2.0: what\u2019s in store for the two ends? https:\/\/www.mckinsey.com\/industries\/industrials-and-electronics\/our-insights\/blockchain-2-0-whats-in-store-for-the-two-ends-semiconductors-suppliers-and-industrials-consumers. Accessed 18 Apr 2023"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL \u2014 Lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19\u201336. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_3","DOI":"10.1007\/3-540-48256-3_3"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Programming Languages and Analysis for Security, pp. 91\u201396. PLAS, ACM (2016). https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with dafny. In: Groote, J.F., Huisman, M. (eds.) Formal Methods for Industrial Critical Systems, pp. 50\u201366. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"11_CR12","unstructured":"Chavez-Dreyfuss, G.: Sweden tests blockchain technology for land registry. https:\/\/www.reuters.com\/article\/us-sweden-blockchain-idUSKCN0Z22KV. Accessed 18 Apr 2023"},{"key":"11_CR13","unstructured":"Clegg, P., Jevans, D.: Cryptocurrency crime and anti-money laundering report. Tech. rep, CipherTrace (2021)"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_16","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Crafa, S., Di Pirro, M., Zucca, E.: Is solidity solid enough? In: Bracciali, A., Clark, J., Pintore, F., R\u00f8nne, P.B., Sala, M. (eds.) FC 2019. LNCS, vol. 11599, pp. 138\u2013153. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43725-1_11","DOI":"10.1007\/978-3-030-43725-1_11"},{"key":"11_CR16","unstructured":"Crosara, M., Centurino, G., Arceri, V.: Towards an operational semantics for solidity. In: van Rooyen, J., Buro, S., Campion, M., Pasqua, M. (eds.) VALID, pp. 1\u20136. IARIA (2019)"},{"issue":"8","key":"11_CR17","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"11_CR18","unstructured":"Ethereum: Solidity. https:\/\/docs.soliditylang.org\/. Accessed 24 May 2023"},{"key":"11_CR19","unstructured":"Gartner. Forecast blockchain business value, worldwide (2019). https:\/\/www.gartner.com\/en\/documents\/3627117. Accessed 04 May 2023"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 161\u2013179. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Jovanovic, D.: Smt-friendly formalization of the Solidity memory model. In: M\u00fcller, P. (ed.) ESOP. LNCS, vol. 12075, pp. 224\u2013250. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_9","DOI":"10.1007\/978-3-030-44914-8_9"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Jiao, J., Kan, S., Lin, S.W., Sanan, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: executable operational semantics of Solidity. In: SP, pp. 1695\u20131712. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00066"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Jiao, J., Lin, S.-W., Sun, J.: A generalized formal semantic framework for smart contracts. In: FASE 2020. LNCS, vol. 12076, pp. 75\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_4","DOI":"10.1007\/978-3-030-45234-6_4"},{"key":"11_CR24","unstructured":"Kelly, J.: Banks adopting blockchain \u2018dramatically faster\u2019 than expected: IBM. https:\/\/www.reuters.com\/article\/us-tech-blockchain-ibm-idUSKCN11Y28D (2016). Accessed 04 May 2023"},{"key":"11_CR25","unstructured":"Llama, D.: Tvl breakdown by smart contract language. https:\/\/defillama.com\/languages (2022)"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Marmsoler, D., Brucker, A.D.: A denotational semantics of solidity in Isabelle\/HOL. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 403\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_23","DOI":"10.1007\/978-3-030-92124-8_23"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Marmsoler, D., Brucker, A.D.: Conformance testing of formal semantics using grammar-based fuzzing. In: Kov\u00e1cs, L., Meinke, K. (eds.) Tests and Proofs, pp. 106\u2013125. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-09827-7_7","DOI":"10.1007\/978-3-031-09827-7_7"},{"key":"11_CR28","unstructured":"Marmsoler, D., Brucker, A.D.: Isabelle\/solidity: a deep embedding of solidity in isabelle\/hol. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Solidity.html. Formal proof development"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Marmsoler, D., Thornton, B.: SSCalc - A Calculus for Solidity Smart Contracts (2023). https:\/\/doi.org\/10.5281\/zenodo.7846232","DOI":"10.5281\/zenodo.7846232"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Matichuk, D., Wenzel, M., Murray, T.: An Isabelle proof method language. In: Klein, G, Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 390\u2013405. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_25","DOI":"10.1007\/978-3-319-08970-6_25"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: correct-by-design smart contracts for Ethereum. In: FC (2019)","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"11_CR32","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-319-89722-6_11"},{"key":"11_CR33","unstructured":"Nakamoto, S.: Bitcoin: A Peer-to-Peer Electronic Cash System (2008)"},{"key":"11_CR34","unstructured":"News, B.: Hackers steal \\$600m in major cryptocurrency heist (2021). https:\/\/www.securityweek.com\/hackers-steal-over-600m-major-crypto-heist. Accessed 04 May 2023"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"11_CR36","unstructured":"Perez, D., Livshits, B.: Smart contract vulnerabilities: vulnerable does not imply exploited. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 1325\u20131341. USENIX Association (2021)"},{"key":"11_CR37","unstructured":"The COQ Development Team. The COQ proof assistant reference manual. LogiCal Project (2004). version 8.0"},{"key":"11_CR38","unstructured":"TNW. These are the top 10 programming languages in blockchain (2019). https:\/\/thenextweb.com\/news\/javascript-programming-java-cryptocurrency. Accessed 04 May 2023"},{"key":"11_CR39","unstructured":"Vogelsteller, F., Buterin, V.: \u201cerc-20: token standard\", ethereum improvement proposals, no. $$20$$ (2015). https:\/\/eips.ethereum.org\/EIPS\/eip-20"},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Monads for functional programming. In: Broy, M. (ed.) Program Design Calculi, pp. 233\u2013264. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-3-662-02880-3_8","DOI":"10.1007\/978-3-662-02880-3_8"},{"key":"11_CR41","doi-asserted-by":"publisher","first-page":"6191537","DOI":"10.1155\/2020\/6191537","volume":"2020","author":"Z Yang","year":"2020","unstructured":"Yang, Z., Lei, H.: Lolisa: Formal syntax and semantics for a subset of the solidity programming language in mathematical tool COQ. Math. Probl. Eng. 2020, 6191537 (2020)","journal-title":"Math. Probl. Eng."},{"key":"11_CR42","unstructured":"YCharts.com. Ethereum transactions per day (2022). https:\/\/ycharts.com\/indicators\/ethereum_transactions_per_day. Accessed 04 May 2023"},{"key":"11_CR43","unstructured":"Yurcan, B.: How blockchain fits into the future of digital identity (2016)"},{"key":"11_CR44","doi-asserted-by":"publisher","unstructured":"Zakrzewski, J.: Towards verification of Ethereum smart contracts. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE. LNCS, vol. 11294, pp. 229\u2013247. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_13","DOI":"10.1007\/978-3-030-03592-1_13"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47115-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,4]],"date-time":"2023-11-04T00:03:37Z","timestamp":1699056217000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47115-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031471148","9783031471155"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47115-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"31 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Eindhoven","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2023\/","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":"41","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":"19","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":"0","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":"46% - 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","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":"4,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)"}}]}}