{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T01:12:52Z","timestamp":1782522772940,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T00:00:00Z","timestamp":1612137600000},"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":[[2021,2]]},"DOI":"10.1145\/3437378.3437879","type":"proceedings-article","created":{"date-parts":[[2021,2,2]],"date-time":"2021-02-02T00:05:57Z","timestamp":1612224357000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":54,"title":["A Survey on Formal Verification for Solidity Smart Contracts"],"prefix":"10.1145","author":[{"given":"Ikram","family":"Garfatta","sequence":"first","affiliation":[{"name":"University of Tunis El Manar Tunisia and University Sorbonne Paris North, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kais","family":"Klai","sequence":"additional","affiliation":[{"name":"University Sorbonne Paris North, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Walid","family":"Gaaloul","sequence":"additional","affiliation":[{"name":"Telecom SudParis, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[{"name":"University of Monastir, Higher Institute for Computer Science and Mathematics, Tunisia and National School for Statistics and Information Analysis, France, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,2]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. Formal Verification for Solidity Contracts \u2014 Ethereum Community Forum. https:\/\/forum.ethereum.org\/discussion\/3779\/formal-verification-for-solidity-contracts.  [n.d.]. Formal Verification for Solidity Contracts \u2014 Ethereum Community Forum. https:\/\/forum.ethereum.org\/discussion\/3779\/formal-verification-for-solidity-contracts."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. Ropsten. https:\/\/ropsten.etherscan.io\/.  [n.d.]. Ropsten. https:\/\/ropsten.etherscan.io\/."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Saswat Anand Corina\u00a0S. Pasareanu and Willem Visser. [n.d.]. Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11 1 ([n.\u00a0d.]).  Saswat Anand Corina\u00a0S. Pasareanu and Willem Visser. [n.d.]. Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11 1 ([n.\u00a0d.]).","DOI":"10.1007\/s10009-008-0090-1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"e_1_3_2_1_6_1","volume-title":"POST 2017, Uppsala, Sweden, April 22-29, 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, Uppsala, Sweden, April 22-29, Proceedings. 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, Uppsala, Sweden, April 22-29, Proceedings."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_1_9_1","volume-title":"5th International Conference, TACAS \u201999","author":"Biere Armin","year":"1999","unstructured":"Armin Biere , Alessandro Cimatti , Edmund\u00a0 M. Clarke , and Yunshan Zhu . 1999 . Symbolic Model Checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems , 5th International Conference, TACAS \u201999 , Held as Part of ETAPS\u201999, Amsterdam, The Netherlands , March 22-28, 1999, Proceedings. 193\u2013207. Armin Biere, Alessandro Cimatti, Edmund\u00a0M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS \u201999, Held as Part of ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings. 193\u2013207."},{"key":"e_1_3_2_1_10_1","volume-title":"Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR abs\/1809.03981(2018).","author":"Brent Lexi","year":"2018","unstructured":"Lexi Brent , Anton Jurisevic , Michael Kong , Eric Liu , Fran\u00e7ois Gauthier , Vincent Gramoli , Ralph Holz , and Bernhard Scholz . 2018 . Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR abs\/1809.03981(2018). Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Fran\u00e7ois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR abs\/1809.03981(2018)."},{"key":"e_1_3_2_1_11_1","volume-title":"CAV 2014, Held as Part of VSL 2014, Austria.","author":"Cavada Roberto","unstructured":"Roberto Cavada , Alessandro Cimatti , Michele Dorigatti , Alberto Griggio , Alessandro Mariotti , Andrea Micheli , Sergio Mover , Marco Roveri , and Stefano Tonetta . [n.d.]. The nuXmv Symbolic Model Checker. In Computer Aided Verification - 26th International Conference , CAV 2014, Held as Part of VSL 2014, Austria. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. [n.d.]. The nuXmv Symbolic Model Checker. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of VSL 2014, Austria."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2017.7884650"},{"key":"e_1_3_2_1_13_1","volume-title":"14th International Conference, TACAS 2008","author":"de Moura Leonardo\u00a0Mendon\u00e7a","year":"2008","unstructured":"Leonardo\u00a0Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner . [n.d.]. Z3 : An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems , 14th International Conference, TACAS 2008 , Budapest, Hungary, March 29- April 6, 2008 . Leonardo\u00a0Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. [n.d.]. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"121","DOI":"10.2991\/ijndc.k.190710.003","article-title":"Defects and Vulnerabilities in Smart Contracts, a Classification using the NIST Bugs Framework","volume":"7","author":"Dingman Wesley","year":"2019","unstructured":"Wesley Dingman , Aviel Cohen , Nick Ferrara , Adam Lynch , Patrick Jasinski , Paul\u00a0 E. Black , and Lin Deng . 2019 . Defects and Vulnerabilities in Smart Contracts, a Classification using the NIST Bugs Framework . IJNDC 7 , 3 (2019), 121 \u2013 132 . Wesley Dingman, Aviel Cohen, Nick Ferrara, Adam Lynch, Patrick Jasinski, Paul\u00a0E. Black, and Lin Deng. 2019. Defects and Vulnerabilities in Smart Contracts, a Classification using the NIST Bugs Framework. IJNDC 7, 3 (2019), 121\u2013132.","journal-title":"IJNDC"},{"key":"e_1_3_2_1_15_1","volume-title":"Solint: A linting utility for Ethereum solidity smart-contracts. https:\/\/github.com\/SilentCicero\/solint.","author":"Dodson Nick","year":"2016","unstructured":"Nick Dodson . 2016 . Solint: A linting utility for Ethereum solidity smart-contracts. https:\/\/github.com\/SilentCicero\/solint. Nick Dodson. 2016. Solint: A linting utility for Ethereum solidity smart-contracts. https:\/\/github.com\/SilentCicero\/solint."},{"key":"e_1_3_2_1_16_1","volume-title":"Advances in Computing and Data Sciences.","author":"Dwivedi Vimal","unstructured":"Vimal Dwivedi , Vipin Deval , Abhishek Dixit , and Alex Norta . 2019. Formal-Verification of Smart-Contract Languages: A Survey . In Advances in Computing and Data Sciences. Singapore , 738\u2013747. Vimal Dwivedi, Vipin Deval, Abhishek Dixit, and Alex Norta. 2019. Formal-Verification of Smart-Contract Languages: A Survey. In Advances in Computing and Data Sciences. Singapore, 738\u2013747."},{"key":"e_1_3_2_1_17_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343\u2013361","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge\u00a0 A. Navas . 2015 . The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343\u2013361 . Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge\u00a0A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343\u2013361."},{"key":"e_1_3_2_1_18_1","unstructured":"Yoichi Hirai. 2017. Ethereum VM for Coq (v0.0.2). https:\/\/medium.com\/@pirapira\/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18.  Yoichi Hirai. 2017. Ethereum VM for Coq (v0.0.2). https:\/\/medium.com\/@pirapira\/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18."},{"key":"e_1_3_2_1_19_1","volume-title":"ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium, NDSS 2018","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 , San Diego, California, USA , February 18-21, 2018. 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, San Diego, California, USA, February 18-21, 2018."},{"key":"e_1_3_2_1_20_1","volume-title":"9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. 553\u2013568","author":"Khurshid Sarfraz","year":"2003","unstructured":"Sarfraz Khurshid , Corina\u00a0 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, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. 553\u2013568 . Sarfraz Khurshid, Corina\u00a0S. 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, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. 553\u2013568."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_22_1","volume-title":"FC 2018, Nieuwpoort, Cura\u00e7ao","author":"Mavridou Anastasia","year":"2018","unstructured":"Anastasia Mavridou and Aron Laszka . [n.d.]. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security - 22nd International Conference , FC 2018, Nieuwpoort, Cura\u00e7ao , February 26 - March 2, 2018 . Anastasia Mavridou and Aron Laszka. [n.d.]. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security - 22nd International Conference, FC 2018, Nieuwpoort, Cura\u00e7ao, February 26 - March 2, 2018."},{"key":"e_1_3_2_1_23_1","volume-title":"FC 2019, Frigate Bay, St. Kitts and Nevis","author":"Mavridou Anastasia","year":"2019","unstructured":"Anastasia Mavridou , Aron Laszka , Emmanouela Stachtiari , and Abhishek Dubey . [n.d.]. VeriSolid : Correct-by-Design Smart Contracts for Ethereum. In Financial Cryptography and Data Security - 23rd International Conference , FC 2019, Frigate Bay, St. Kitts and Nevis , February 18-22, 2019 . Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. [n.d.]. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Financial Cryptography and Data Security - 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis, February 18-22, 2019."},{"key":"e_1_3_2_1_24_1","volume-title":"Symbolic model checking","author":"McMillan L.","unstructured":"Kenneth\u00a0 L. McMillan . 1993. Symbolic model checking . Kluwer . Kenneth\u00a0L. McMillan. 1993. Symbolic model checking. Kluwer."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855768.1855773"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_27_1","volume-title":"CAV 2014","author":"Rakamaric Zvonimir","year":"2014","unstructured":"Zvonimir Rakamaric and Michael Emmi . [n.d.]. SMACK : Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference , CAV 2014 , Vienna, Austria , July 18-22, 2014 . Zvonimir Rakamaric and Michael Emmi. [n.d.]. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference, CAV 2014, Vienna, Austria, July 18-22, 2014."},{"key":"e_1_3_2_1_28_1","unstructured":"Alex Rea. 2016-2020. SolCover: Code coverage for Solidity smart-contracts. https:\/\/github.com\/sc-forks\/solidity-coverage.  Alex Rea. 2016-2020. SolCover: Code coverage for Solidity smart-contracts. https:\/\/github.com\/sc-forks\/solidity-coverage."},{"key":"e_1_3_2_1_29_1","volume-title":"NFM 2012, USA, April 3-5, 2012. Proceedings.","author":"Tinelli Cesare","year":"2012","unstructured":"Cesare Tinelli . 2012 . SMT-Based Model Checking. In NASA Formal Methods - 4th International Symposium , NFM 2012, USA, April 3-5, 2012. Proceedings. Cesare Tinelli. 2012. SMT-Based Model Checking. In NASA Formal Methods - 4th International Symposium, NFM 2012, USA, April 3-5, 2012. Proceedings."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_1_32_1","volume-title":"Security Assurance for Smart Contract. In 9th IFIP International Conference on New Technologies, Mobility and Security, NTMS 2018","author":"Zhou Ence","year":"2018","unstructured":"Ence Zhou , Song Hua , Bingfeng Pi , Jun Sun , Yashihide Nomura , Kazuhiro Yamashita , and Hidetoshi Kurihara . 2018 . Security Assurance for Smart Contract. In 9th IFIP International Conference on New Technologies, Mobility and Security, NTMS 2018 , Paris, France , February 26-28, 2018. 1\u20135. Ence Zhou, Song Hua, Bingfeng Pi, Jun Sun, Yashihide Nomura, Kazuhiro Yamashita, and Hidetoshi Kurihara. 2018. Security Assurance for Smart Contract. In 9th IFIP International Conference on New Technologies, Mobility and Security, NTMS 2018, Paris, France, February 26-28, 2018. 1\u20135."}],"event":{"name":"ACSW '21: 2021 Australasian Computer Science Week Multiconference","location":"Dunedin New Zealand","acronym":"ACSW '21"},"container-title":["2021 Australasian Computer Science Week Multiconference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437378.3437879","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437378.3437879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:25Z","timestamp":1750191445000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437378.3437879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2]]},"references-count":32,"alternative-id":["10.1145\/3437378.3437879","10.1145\/3437378"],"URL":"https:\/\/doi.org\/10.1145\/3437378.3437879","relation":{},"subject":[],"published":{"date-parts":[[2021,2]]},"assertion":[{"value":"2021-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}