{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T05:17:00Z","timestamp":1781327820757,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T00:00:00Z","timestamp":1650844800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,4,25]]},"DOI":"10.1145\/3477314.3507309","type":"proceedings-article","created":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T00:37:36Z","timestamp":1651883856000},"page":"316-325","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Model checking of vulnerabilities in smart contracts"],"prefix":"10.1145","author":[{"given":"Ikram","family":"Garfatta","sequence":"first","affiliation":[{"name":"University of Tunis El Manar, Tunis, Tunisia and University Sorbonne Paris North, Villetaneuse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ka\u00efs","family":"Klai","sequence":"additional","affiliation":[{"name":"University Sorbonne Paris North, Villetaneuse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed","family":"Gra\u00efet","sequence":"additional","affiliation":[{"name":"University of Monastir, Monastir, Tunisia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Walid","family":"Gaaloul","sequence":"additional","affiliation":[{"name":"T\u00e9l\u00e9com SudParis, \u00c9vry, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,5,6]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. Solidity documentation. https:\/\/docs.soliditylang.org\/en\/latest\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220903.3221139"},{"key":"e_1_3_2_1_4_1","volume-title":"POST 2017, Held as Part of the ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings.","author":"Atzei Nicola","unstructured":"Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. [n. d.]. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Principles of Security and Trust - 6th International Conference, POST 2017, Held as Part of the ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2017.7884650"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2020.2977594"},{"key":"e_1_3_2_1_8_1","volume-title":"Applications and Theory of Petri Nets","author":"Evangelista Sami","year":"2005","unstructured":"Sami Evangelista. 2005. High Level Petri Nets Analysis with Helena. In Applications and Theory of Petri Nets 2005. Berlin, 455--464."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437378.3437879"},{"key":"e_1_3_2_1_10_1","volume-title":"OTM 2018 Conferences - Confederated International Conferences: CoopIS, C&TC, and ODBASE 2018, Valletta, Malta, October 22--26, 2018, Proceedings, Part I (Lecture Notes in Computer Science)","volume":"11229","author":"Garfatta Ikram","year":"2018","unstructured":"Ikram Garfatta, Kais Klai, Mohamed Graiet, and Walid Gaaloul. 2018. Formal Modelling and Verification of Cloud Resource Allocation in Business Processes. In On the Move to Meaningful Internet Systems. OTM 2018 Conferences - Confederated International Conferences: CoopIS, C&TC, and ODBASE 2018, Valletta, Malta, October 22--26, 2018, Proceedings, Part I (Lecture Notes in Computer Science), Vol. 11229. Springer, 552--567."},{"key":"e_1_3_2_1_11_1","volume-title":"Service-Oriented Computing- ICSOC 2020 Workshops - PhD symposium, Dubai, United Arab Emirates, December 14--17","author":"Garfatta Ikram","year":"2020","unstructured":"Ikram Garfatta, Ka\u00efs Klai, Mahamed Gra\u00efet, and Walid Gaaloul. 2020. Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. In Service-Oriented Computing- ICSOC 2020 Workshops - PhD symposium, Dubai, United Arab Emirates, December 14--17, 2020, Proceedings (Lecture Notes in Computer Science), Vol. 12632. Springer, 47--53."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE53228.2021.00024"},{"key":"e_1_3_2_1_13_1","volume-title":"International Conference on Application and Theory of Petri Nets. 342--416","author":"Jensen Kurt","year":"1989","unstructured":"Kurt Jensen. 1989. Coloured Petri nets: A high level language for system design and analysis. In International Conference on Application and Theory of Petri Nets. 342--416."},{"key":"e_1_3_2_1_14_1","volume-title":"Kristensen","author":"Jensen Kurt","year":"2009","unstructured":"Kurt Jensen and Lars M. Kristensen. 2009. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer Publishing Company, Incorporated."},{"key":"e_1_3_2_1_15_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."},{"key":"e_1_3_2_1_16_1","volume-title":"9th International Conference, TACAS 2003, Poland, April 7--11, Proceedings.","author":"Khurshid Sarfraz","year":"2003","unstructured":"Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Poland, April 7--11, Proceedings."},{"key":"e_1_3_2_1_17_1","volume-title":"29th International Conference, PETRI NETS 2008, Xi'an, China, June 23--27, 2008. Proceedings. 288--306","author":"Klai Kais","year":"2008","unstructured":"Kais Klai and Denis Poitrenaud. 2008. MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. In Applications and Theory of Petri Nets, 29th International Conference, PETRI NETS 2008, Xi'an, China, June 23--27, 2008. Proceedings. 288--306."},{"key":"e_1_3_2_1_18_1","volume-title":"43rd IEEE COMPSAC. 555--560.","author":"Liu Zhen-Tian","unstructured":"Zhen-Tian Liu and Jing Liu. 2019. Formal Verification of Blockchain Smart Contract Based on Colored Petri Net Models. In 43rd IEEE COMPSAC. 555--560."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_20_1","volume-title":"FC 2019, St. Kitts and Nevis, February 18--22","author":"Mavridou Anastasia","year":"2019","unstructured":"Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. 2019. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Financial Cryptography and Data Security - 23rd International Conference, FC 2019, St. Kitts and Nevis, February 18--22, 2019. 446--465."},{"key":"e_1_3_2_1_21_1","volume-title":"Definition of standard ML","author":"Milner Robin","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. 1990. Definition of standard ML. MIT Press."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244002.1244309"},{"key":"e_1_3_2_1_24_1","volume-title":"The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science, Providence. IEEE Computer Society, 46--57","author":"Pnueli Amir","year":"1977","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science, Providence. IEEE Computer Society, 46--57."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"e_1_3_2_1_26_1","volume-title":"Data61 (CSIRO)","author":"Staples M.","unstructured":"M. Staples, S. Chen, Sara Falamaki, A. Ponomarev, Paul Rimba, A. Tran, I. Weber, Sherry Xu, and John Zhu. 2017. Risks and opportunities for systems using blockchain and smart contracts. In Data61 (CSIRO), Sydney."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 12th International Conference on Applications and Theory of Petri Nets.","author":"Van Hee KM","year":"1991","unstructured":"KM Van Hee and PAC Verkoulen. 1991. Integration of a data model and high-level petri nets. In Proceedings of the 12th International Conference on Applications and Theory of Petri Nets."}],"event":{"name":"SAC '22: The 37th ACM\/SIGAPP Symposium on Applied Computing","location":"Virtual Event","acronym":"SAC '22","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"]},"container-title":["Proceedings of the 37th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3507309","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477314.3507309","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:30Z","timestamp":1750188630000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477314.3507309"}},"subtitle":["a solidity-to-CPN approach"],"short-title":[],"issued":{"date-parts":[[2022,4,25]]},"references-count":28,"alternative-id":["10.1145\/3477314.3507309","10.1145\/3477314"],"URL":"https:\/\/doi.org\/10.1145\/3477314.3507309","relation":{},"subject":[],"published":{"date-parts":[[2022,4,25]]},"assertion":[{"value":"2022-05-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}