{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:00:15Z","timestamp":1776553215386,"version":"3.51.2"},"publisher-location":"Singapore","reference-count":30,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819789429","type":"print"},{"value":"9789819789436","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_15","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"305-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7524-4497","authenticated-orcid":false,"given":"Thi Thu Ha","family":"Doan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9000-1239","authenticated-orcid":false,"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 66\u201377 (2018). https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Anton, P., Dimitar, D., Petar, T., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1661\u20131677 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"15_CR3","unstructured":"Arvay, B., Doan, T.T.H., Thiemann, P.: A dynamic logic for symbolic execution for the smart contract programming language michelson. In: European Conference on Object-Oriented Programming (ECOOP 2024). To appear (2024)"},{"key":"15_CR4","unstructured":"Erc20 api: An Attack Vector on the Approve\/Transferfrom Methods. https:\/\/docs.google.com\/document\/d\/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM\/edit#heading=h.m9fhqynw2xvt"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, 7\u201311 Oct 2019, Revised Selected Papers, Part I. Lecture Notes in Computer Science, vol. 12232, pp. 368\u2013379. Springer, Heidelberg (2019)","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"15_CR6","unstructured":"Buterin, V.: A Next-Generation Smart Contract and Decentralized Application Platform (2013). https:\/\/ethereum.org\/en\/whitepaper\/"},{"key":"15_CR7","unstructured":"Understanding the DAO Attack. https:\/\/www.coindesk.com\/learn\/understanding-the-dao-attack\/"},{"key":"15_CR8","unstructured":"ERC-20. https:\/\/ethereum.org\/en\/developers\/docs\/standards\/tokens\/erc-20"},{"key":"15_CR9","unstructured":"FA1.2 Tokens. https:\/\/docs.tezos.com\/architecture\/tokens\/FA1.2"},{"key":"15_CR10","unstructured":"Goodman, L.: Tezos-a Self-amending Crypto-Ledger (2014). https:\/\/www.tezos.com\/static\/papers\/white-paper.pdf"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Hajdu, A., Jovanovio, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 161\u2013179. Springer International Publishing (2020)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 204\u2013217 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Financial Cryptography and Data Security, pp. 520\u2013535. Springer International Publishing (2017)","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"15_CR14","unstructured":"Kolibri Oracle Contract. https:\/\/kolibri.finance\/docs\/components\/oracle"},{"key":"15_CR15","unstructured":"Ligo: Smart Contract Language for Tezos. https:\/\/ligolang.org\/"},{"key":"15_CR16","unstructured":"Liquidity. https:\/\/liquidity-lang.org\/"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"15_CR18","unstructured":"Michelson: The Language of Smart Contracts in Tezos. https:\/\/tezos.gitlab.io\/alpha\/michelson.html"},{"key":"15_CR19","unstructured":"Michelson Reference. https:\/\/tezos.gitlab.io\/michelson-reference\/"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., Dinaburg, A.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts. In: 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1186\u20131189 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00133","DOI":"10.1109\/ASE.2019.00133"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008)"},{"key":"15_CR22","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-981-99-7584-6_2","volume-title":"Formal Methods and Software Engineering","author":"TD Nguyen","year":"2023","unstructured":"Nguyen, T.D., Pham, L.H., Sun, J., Le, Q.L.: An idealist\u2019s approach for smart contract correctness. In: Li, Y., Tahar, S. (eds.) Formal Methods and Software Engineering, pp. 11\u201328. Springer Nature Singapore, Singapore (2023)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s00354-022-00167-1","volume":"40","author":"Y Nishida","year":"2022","unstructured":"Nishida, Y., Saito, H., Chen, R., Kawata, A., Furuse, J., Suenaga, K., Igarashi, A.: HELMHOLTZ: a verifier for Tezos smart contracts based on refinement types. N. Gener. Comput. 40, 507\u2013540 (2022). https:\/\/doi.org\/10.1007\/s00354-022-00167-1","journal-title":"N. Gener. Comput."},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Rou, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 912\u2013915 (2018). https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"15_CR25","unstructured":"SCV: A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution. https:\/\/zenodo.org\/records\/11363663"},{"key":"15_CR26","unstructured":"SmartPy: Smart Contracts on Tezos. https:\/\/smartpy.io\/"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.: Securify: Practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 67\u201382 (2018). https:\/\/doi.org\/10.1145\/3243734.3243780","DOI":"10.1145\/3243734.3243780"},{"key":"15_CR28","unstructured":"Tzstats: USDtz. https:\/\/tzstats.com\/KT1LN4LPSqTMS7Sd2CJw4bbDGRkMv2t68Fy9"},{"key":"15_CR29","unstructured":"USDtz Whitepaper. https:\/\/docs.usdtz.com\/usdtz-whitepaper"},{"key":"15_CR30","unstructured":"The Parity Wallet Hack Explained. https:\/\/blog.openzeppelin.com\/on-the-parity-wallet-multisig-hack-405a8c12e8f7"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:36Z","timestamp":1748364756000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}