{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T10:34:12Z","timestamp":1763202852352,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T00:00:00Z","timestamp":1712534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,8]]},"DOI":"10.1145\/3605098.3636040","type":"proceedings-article","created":{"date-parts":[[2024,5,21]],"date-time":"2024-05-21T17:59:16Z","timestamp":1716314356000},"page":"1425-1432","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Modeling and verification of smart contracts with Abstract State Machines"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9756-4675","authenticated-orcid":false,"given":"Chiara","family":"Braghin","sequence":"first","affiliation":[{"name":"Computer Science Department, Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1400-1026","authenticated-orcid":false,"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5956-3945","authenticated-orcid":false,"given":"Simone","family":"Valentini","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universit\u00e0 degli Studi di Milano, Milan, Italy"}]}],"member":"320","published-online":{"date-parts":[[2024,5,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"N. Alchemy. 2019. A short history of smart contract hacks on ethereum: A.k.a. why you need a smart contract security audit."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.24251\/HICSS.2020.650"},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. of the 7th Int. Conf. on Certified Programs and Proofs (CPP18)","volume":"77","author":"Amani Sidney","year":"2018","unstructured":"Sidney Amani, Myriam B\u00e9gel, Maksym Bortin, and Mark Staples. 2018. Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In Proc. of the 7th Int. Conf. on Certified Programs and Proofs (CPP18), Vol. 2018-. ACM, 66--77."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1019"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. Series. ACM, 322--326","author":"Bai Xiaomin","year":"2018","unstructured":"Xiaomin Bai, Zijing Cheng, Zhangbo Duan, and Kai Hu. 2018. Formal Modeling and Verification of Smart Contracts. In ACM Int. Conf. Proc. Series. ACM, 322--326."},{"volume-title":"Proc. of the ACM Workshop on Programming Languages and Analysis for Security (PLAS16)","author":"Bhargavan Karthikeyan","key":"e_1_3_2_1_6_1","unstructured":"Karthikeyan Bhargavan, Antoine Delignat-Lavaud, and C\u00e9dric Fournet et al. 2016. Formal Verification of Smart Contracts: Short Paper. In Proc. of the ACM Workshop on Programming Languages and Analysis for Security (PLAS16). ACM, 91--96."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-56641-1"},{"volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"B\u00f6rger Egon","key":"e_1_3_2_1_8_1","unstructured":"Egon B\u00f6rger and Robert St\u00e4rk. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer Verlag."},{"key":"e_1_3_2_1_9_1","unstructured":"E. Foundation. 2017. Ethereum."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437378.3437879"},{"key":"e_1_3_2_1_11_1","volume-title":"ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium (NDSS","author":"Kalra Sukrit","year":"2018","unstructured":"Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium (NDSS 2018)."},{"key":"e_1_3_2_1_12_1","volume-title":"Securing Smart Contracts in Blockchain. In 34th IEEE-ACM Int. Conf. on Automated Software Engineering Workshops (ASEW","author":"Kongmanee Jaturong","year":"2019","unstructured":"Jaturong Kongmanee, Phongphun Kijsanayothin, and Rattikorn Hewett. 2019. Securing Smart Contracts in Blockchain. In 34th IEEE-ACM Int. Conf. on Automated Software Engineering Workshops (ASEW 2019). IEEE, 69--76."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_14_1","volume-title":"Formal Verification of Smart Contracts Using Interface Automata. In IEEE Int. Conf. on Blockchain. 556--563","author":"Madl Gabor","year":"2019","unstructured":"Gabor Madl, Luis Bathen, German Flores, and Divyesh Jadav. 2019. Formal Verification of Smart Contracts Using Interface Automata. In IEEE Int. Conf. on Blockchain. 556--563."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security. 523--540.","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_17_1","first-page":"28","article-title":"Smart contracts: building blocks for digital markets. EXTROPY","volume":"18","author":"Szabo Nick","year":"1996","unstructured":"Nick Szabo. 1996. Smart contracts: building blocks for digital markets. EXTROPY: The Journal of Transhumanist Thought,(16) 18, 2 (1996), 28.","journal-title":"The Journal of Transhumanist Thought,(16)"},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. Series. 664--676","author":"Torres Christof Ferreira","year":"2018","unstructured":"Christof Ferreira Torres, Julian Sch\u00fctte, and Radu State. 2018. Osiris: Hunting for integer bugs in ethereum smart contracts. In ACM Int. Conf. Proc. Series. 664--676."}],"event":{"name":"SAC '24: 39th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Avila Spain","acronym":"SAC '24"},"container-title":["Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605098.3636040","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3605098.3636040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:59Z","timestamp":1750291439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605098.3636040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,8]]},"references-count":18,"alternative-id":["10.1145\/3605098.3636040","10.1145\/3605098"],"URL":"https:\/\/doi.org\/10.1145\/3605098.3636040","relation":{},"subject":[],"published":{"date-parts":[[2024,4,8]]},"assertion":[{"value":"2024-05-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}