{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T04:48:15Z","timestamp":1767156495636,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T00:00:00Z","timestamp":1679875200000},"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":[[2023,3,27]]},"DOI":"10.1145\/3555776.3578996","type":"proceedings-article","created":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T17:16:29Z","timestamp":1686158189000},"page":"262-269","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards automated verification of Bitcoin-based decentralised applications"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7411-9678","authenticated-orcid":false,"given":"Stefano","family":"Bistarelli","sequence":"first","affiliation":[{"name":"Universita di Perugia, Perugia, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1451-9260","authenticated-orcid":false,"given":"Andrea","family":"Bracciali","sequence":"additional","affiliation":[{"name":"University of Stirling, Stirling, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7535-2284","authenticated-orcid":false,"given":"Rick","family":"Klomp","sequence":"additional","affiliation":[{"name":"TZ Connect, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9774-1600","authenticated-orcid":false,"given":"Ivan","family":"Mercanti","sequence":"additional","affiliation":[{"name":"University of Perugia, Perugia, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,7]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LIPIcs","first-page":"1","volume-title":"TYPES","author":"Alhabardi Fahad F.","year":"2021","unstructured":"Fahad F. Alhabardi , Arnold Beckmann , Bogdan Lazar , and Anton Setzer . Verification of bitcoin script in agda using weakest preconditions for access control . In TYPES , volume 239 of LIPIcs , pages 1: 1 -- 1 :25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 2021 . Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of bitcoin script in agda using weakest preconditions for access control. In TYPES, volume 239 of LIPIcs, pages 1:1--1:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021."},{"key":"e_1_3_2_1_2_1","first-page":"443","volume-title":"IEEE Symposium on Security and Privacy","author":"Andrychowicz Marcin","year":"2014","unstructured":"Marcin Andrychowicz , Stefan Dziembowski , Daniel Malinowski , and Lukasz Mazurek . Secure multiparty computations on bitcoin . In IEEE Symposium on Security and Privacy , pages 443 -- 458 . IEEE Computer Society , 2014 . Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Lukasz Mazurek. Secure multiparty computations on bitcoin. In IEEE Symposium on Security and Privacy, pages 443--458. IEEE Computer Society, 2014."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","first-page":"770503","DOI":"10.3389\/fbloc.2021.770503","article-title":"Is it possible to verify if a transaction is spendable?","volume":"4","author":"Arenas Marcelo","year":"2021","unstructured":"Marcelo Arenas , Thomas Reisenegger , Juan L. Reutter , and Domagoj Vrgoc . Is it possible to verify if a transaction is spendable? Frontiers Blockchain , 4 : 770503 , 2021 . Marcelo Arenas, Thomas Reisenegger, Juan L. Reutter, and Domagoj Vrgoc. Is it possible to verify if a transaction is spendable? Frontiers Blockchain, 4:770503, 2021.","journal-title":"Frontiers Blockchain"},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-319-89722-6_9","volume-title":"POST","author":"Atzei Nicola","year":"2018","unstructured":"Nicola Atzei , Massimo Bartoletti , Tiziana Cimoli , Stefano Lande , and Roberto Zunino . Sok: Unraveling bitcoin smart contracts . In POST , volume 10804 of Lecture Notes in Computer Science , pages 217 -- 242 . Springer , 2018 . Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande, and Roberto Zunino. Sok: Unraveling bitcoin smart contracts. In POST, volume 10804 of Lecture Notes in Computer Science, pages 217--242. Springer, 2018."},{"key":"e_1_3_2_1_5_1","first-page":"1124","volume-title":"ESEC\/SIGSOFT FSE","author":"Atzei Nicola","year":"2019","unstructured":"Nicola Atzei , Massimo Bartoletti , Stefano Lande , Nobuko Yoshida , and Roberto Zunino . Developing secure bitcoin contracts with bitml . In ESEC\/SIGSOFT FSE , pages 1124 -- 1128 . ACM, 2019 . Nicola Atzei, Massimo Bartoletti, Stefano Lande, Nobuko Yoshida, and Roberto Zunino. Developing secure bitcoin contracts with bitml. In ESEC\/SIGSOFT FSE, pages 1124--1128. ACM, 2019."},{"key":"e_1_3_2_1_6_1","volume-title":"Pikachu: Securing pos blockchains from long-range attacks by checkpointing into bitcoin pow using taproot. CoRR, abs\/2208.05408","author":"Azouvi Sarah","year":"2022","unstructured":"Sarah Azouvi and Marko Vukolic . Pikachu: Securing pos blockchains from long-range attacks by checkpointing into bitcoin pow using taproot. CoRR, abs\/2208.05408 , 2022 . Sarah Azouvi and Marko Vukolic. Pikachu: Securing pos blockchains from long-range attacks by checkpointing into bitcoin pow using taproot. CoRR, abs\/2208.05408, 2022."},{"key":"e_1_3_2_1_7_1","first-page":"93","volume-title":"CVCBT","author":"Bistarelli Stefano","year":"2018","unstructured":"Stefano Bistarelli , Ivan Mercanti , and Francesco Santini . An analysis of non-standard bitcoin transactions . In CVCBT , pages 93 -- 96 . IEEE, 2018 . Stefano Bistarelli, Ivan Mercanti, and Francesco Santini. An analysis of non-standard bitcoin transactions. In CVCBT, pages 93--96. IEEE, 2018."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.3389\/fbloc.2019.00007"},{"key":"e_1_3_2_1_9_1","first-page":"104","volume-title":"IEEE Symposium on Security and Privacy","author":"Bonneau Joseph","year":"2015","unstructured":"Joseph Bonneau , Andrew Miller , Jeremy Clark , Arvind Narayanan , Joshua A. Kroll , and Edward W. Felten . Sok: Research perspectives and challenges for bitcoin and cryptocurrencies . In IEEE Symposium on Security and Privacy , pages 104 -- 121 . IEEE Computer Society , 2015 . Joseph Bonneau, Andrew Miller, Jeremy Clark, Arvind Narayanan, Joshua A. Kroll, and Edward W. Felten. Sok: Research perspectives and challenges for bitcoin and cryptocurrencies. In IEEE Symposium on Security and Privacy, pages 104--121. IEEE Computer Society, 2015."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Harris Brakmi\u0107. Bitcoin Script pages 201--224. Apress Berkeley CA 2019.  Harris Brakmi\u0107. Bitcoin Script pages 201--224. Apress Berkeley CA 2019.","DOI":"10.1007\/978-1-4842-5522-3_7"},{"key":"e_1_3_2_1_11_1","first-page":"87","volume-title":"CloudNet","author":"Casas Pedro","year":"2021","unstructured":"Pedro Casas , Matteo Romiti , Peter Holzer , Sami Ben Mariem , Benoit Donnet , and Bernhard Haslhofer . Where is the light(ning) in the taproot dawn? unveiling the bitcoin lightning (IP) network . In CloudNet , pages 87 -- 90 . IEEE, 2021 . Pedro Casas, Matteo Romiti, Peter Holzer, Sami Ben Mariem, Benoit Donnet, and Bernhard Haslhofer. Where is the light(ning) in the taproot dawn? unveiling the bitcoin lightning (IP) network. In CloudNet, pages 87--90. IEEE, 2021."},{"key":"e_1_3_2_1_12_1","volume-title":"Bitcoin trace-net: Formal contract verification at signing time. CoRR, abs\/2007.07528","author":"Chiang James","year":"2020","unstructured":"James Chiang . Bitcoin trace-net: Formal contract verification at signing time. CoRR, abs\/2007.07528 , 2020 . James Chiang. Bitcoin trace-net: Formal contract verification at signing time. CoRR, abs\/2007.07528, 2020."},{"key":"e_1_3_2_1_13_1","first-page":"801","volume-title":"USENIX Security Symposium","author":"Das Poulami","year":"2019","unstructured":"Poulami Das , Lisa Eckey , Tommaso Frassetto , David Gens , Kristina Host\u00e1kov\u00e1 , Patrick Jauernig , Sebastian Faust , and Ahmad-Reza Sadeghi . Fastkitten : Practical smart contracts on bitcoin . In USENIX Security Symposium , pages 801 -- 818 . USENIX Association , 2019 . Poulami Das, Lisa Eckey, Tommaso Frassetto, David Gens, Kristina Host\u00e1kov\u00e1, Patrick Jauernig, Sebastian Faust, and Ahmad-Reza Sadeghi. Fastkitten: Practical smart contracts on bitcoin. In USENIX Security Symposium, pages 801--818. USENIX Association, 2019."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46803-6_10"},{"key":"e_1_3_2_1_15_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-030-00305-0_3","volume-title":"DPM\/CBT@ESORICS","author":"Klomp Rick","year":"2018","unstructured":"Rick Klomp and Andrea Bracciali . On symbolic verification of bitcoin's script language . In DPM\/CBT@ESORICS , volume 11025 of Lecture Notes in Computer Science , pages 38 -- 56 . Springer , 2018 . Rick Klomp and Andrea Bracciali. On symbolic verification of bitcoin's script language. In DPM\/CBT@ESORICS, volume 11025 of Lecture Notes in Computer Science, pages 38--56. Springer, 2018."},{"key":"e_1_3_2_1_16_1","first-page":"16","volume-title":"AFT","author":"McCorry Patrick","year":"2019","unstructured":"Patrick McCorry , Surya Bakshi , Iddo Bentov , Sarah Meiklejohn , and Andrew Miller . Pisa : Arbitration outsourcing for state channels . In AFT , pages 16 -- 30 . ACM, 2019 . Patrick McCorry, Surya Bakshi, Iddo Bentov, Sarah Meiklejohn, and Andrew Miller. Pisa: Arbitration outsourcing for state channels. In AFT, pages 16--30. ACM, 2019."},{"key":"e_1_3_2_1_17_1","volume-title":"Financial Cryptography Workshops","volume":"9604","author":"M\u00f6ser Malte","year":"2016","unstructured":"Malte M\u00f6ser , Ittay Eyal , and Emin G\u00fcn Sirer . Bitcoin covenants . In Financial Cryptography Workshops , volume 9604 of Lecture Notes in Computer Science, pages 126--141. Springer , 2016 . Malte M\u00f6ser, Ittay Eyal, and Emin G\u00fcn Sirer. Bitcoin covenants. In Financial Cryptography Workshops, volume 9604 of Lecture Notes in Computer Science, pages 126--141. Springer, 2016."},{"key":"e_1_3_2_1_18_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system. Bitcoin project white paper","author":"Nakamoto Satoshi","year":"2009","unstructured":"Satoshi Nakamoto . Bitcoin: A peer-to-peer electronic cash system. Bitcoin project white paper , 2009 . Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. Bitcoin project white paper, 2009."}],"event":{"name":"SAC '23: 38th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Tallinn Estonia","acronym":"SAC '23"},"container-title":["Proceedings of the 38th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555776.3578996","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3555776.3578996","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:36Z","timestamp":1750182696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3555776.3578996"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,27]]},"references-count":18,"alternative-id":["10.1145\/3555776.3578996","10.1145\/3555776"],"URL":"https:\/\/doi.org\/10.1145\/3555776.3578996","relation":{},"subject":[],"published":{"date-parts":[[2023,3,27]]},"assertion":[{"value":"2023-06-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}