{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:22:14Z","timestamp":1757542934788,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,30]],"date-time":"2022-05-30T00:00:00Z","timestamp":1653868800000},"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,5,30]]},"DOI":"10.1145\/3494106.3528672","type":"proceedings-article","created":{"date-parts":[[2022,5,24]],"date-time":"2022-05-24T04:08:26Z","timestamp":1653365306000},"page":"3-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Vulnerable Smart Contract Detection by Means of Model Checking"],"prefix":"10.1145","author":[{"given":"Giuseppe","family":"Crincoli","sequence":"first","affiliation":[{"name":"Institute for Informatics and Telematics, CNR, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giacomo","family":"Iadarola","sequence":"additional","affiliation":[{"name":"Institute for Informatics and Telematics, CNR, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piera Elena","family":"La Rocca","sequence":"additional","affiliation":[{"name":"Institute for Informatics and Telematics, CNR, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Martinelli","sequence":"additional","affiliation":[{"name":"Institute for Informatics and Telematics, CNR, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Mercaldo","sequence":"additional","affiliation":[{"name":"University of Molise &amp; Institute for Informatics and Telematics, CNR, Campobasso, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonella","family":"Santone","sequence":"additional","affiliation":[{"name":"University of Molise, Campobasso, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,5,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.21744\/lingcure.v5nS3.1629"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_3_2_1_3_1","first-page":"21","article-title":"Formal methods: Benefits, challenges and future direction","volume":"4","author":"Batra Mona","year":"2013","unstructured":"Mona Batra . 2013 . Formal methods: Benefits, challenges and future direction . Journal of Global Research in Computer Science 4 , 5 (2013), 21 -- 25 . Mona Batra. 2013. Formal methods: Benefits, challenges and future direction. Journal of Global Research in Computer Science 4, 5 (2013), 21--25.","journal-title":"Journal of Global Research in Computer Science"},{"key":"e_1_3_2_1_4_1","first-page":"2005","article-title":"Introducing formal methods into industry using Cleanroom and CSP","volume":"1","author":"Broadfoot Guy H","year":"2011","unstructured":"Guy H Broadfoot and PJ Hopcroft . 2011 . Introducing formal methods into industry using Cleanroom and CSP . Dedicated Systems Magazine Q 1 (2011), 2005 . Guy H Broadfoot and PJ Hopcroft. 2011. Introducing formal methods into industry using Cleanroom and CSP. Dedicated Systems Magazine Q 1 (2011), 2005.","journal-title":"Dedicated Systems Magazine Q"},{"key":"e_1_3_2_1_5_1","volume-title":"Formal methods for prostate cancer Gleason score and treatment prediction using radiomic biomarkers. Magnetic resonance imaging 66","author":"Brunese Luca","year":"2020","unstructured":"Luca Brunese , Francesco Mercaldo , Alfonso Reginelli , and Antonella Santone . 2020. Formal methods for prostate cancer Gleason score and treatment prediction using radiomic biomarkers. Magnetic resonance imaging 66 ( 2020 ), 165--175. Luca Brunese, Francesco Mercaldo, Alfonso Reginelli, and Antonella Santone. 2020. Formal methods for prostate cancer Gleason score and treatment prediction using radiomic biomarkers. Magnetic resonance imaging 66 (2020), 165--175."},{"key":"e_1_3_2_1_6_1","unstructured":"Vitalik Buterin et al. 2014. A next-generation smart contract and decentralized application platform. white paper 3 37 (2014).  Vitalik Buterin et al. 2014. A next-generation smart contract and decentralized application platform. white paper 3 37 (2014)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.1993-4516"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2019.101691"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE.2017.23"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2017.3421554"},{"key":"e_1_3_2_1_11_1","first-page":"669","article-title":"Realising the Benefits of Formal Methods","volume":"13","author":"Hall Anthony","year":"2007","unstructured":"Anthony Hall . 2007 . Realising the Benefits of Formal Methods . J. Univers. Comput. Sci. 13 , 5 (2007), 669 -- 678 . Anthony Hall. 2007. Realising the Benefits of Formal Methods. J. Univers. Comput. Sci. 13, 5 (2007), 669--678.","journal-title":"J. Univers. Comput. Sci."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipm.2020.102462"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/IOTSMS48152.2019.8939172"},{"key":"e_1_3_2_1_14_1","unstructured":"Nomura Research Institute. 2015. Survey on Blockchain Technologies and Related Services.  Nomura Research Institute. 2015. Survey on Blockchain Technologies and Related Services."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2018.04.008"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4018\/JCIT.2019010102"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE.2019.00057"},{"key":"e_1_3_2_1_20_1","unstructured":"nccgroup. 2018. DASP Top Ten. Accessed: Nov-2021.  nccgroup. 2018. DASP Top Ten. Accessed: Nov-2021."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2970495"},{"key":"e_1_3_2_1_23_1","unstructured":"Christof Ferreira Torres Mathis Steichen etal 2019. The art of the scam: De- mystifying honeypots in ethereum smart contracts. In 28th {USENIX} security symposium ({USENIX} security 19). 1591--1607.  Christof Ferreira Torres Mathis Steichen et al. 2019. The art of the scam: De- mystifying honeypots in ethereum smart contracts. In 28th {USENIX} security symposium ({USENIX} security 19). 1591--1607."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Yuan Zhuang Zhenguang Liu Peng Qian Qi Liu Xiang Wang and Qinming He. 2020. Smart Contract Vulnerability Detection using Graph Neural Network.. In IJCAI. 3283--3290  Yuan Zhuang Zhenguang Liu Peng Qian Qi Liu Xiang Wang and Qinming He. 2020. Smart Contract Vulnerability Detection using Graph Neural Network.. In IJCAI. 3283--3290","DOI":"10.24963\/ijcai.2020\/454"}],"event":{"name":"ASIA CCS '22: ACM Asia Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Nagasaki Japan","acronym":"ASIA CCS '22"},"container-title":["Proceedings of the Fourth ACM International Symposium on Blockchain and Secure Critical Infrastructure"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3494106.3528672","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3494106.3528672","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:44Z","timestamp":1750188644000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3494106.3528672"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,30]]},"references-count":25,"alternative-id":["10.1145\/3494106.3528672","10.1145\/3494106"],"URL":"https:\/\/doi.org\/10.1145\/3494106.3528672","relation":{},"subject":[],"published":{"date-parts":[[2022,5,30]]},"assertion":[{"value":"2022-05-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}