{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T05:19:35Z","timestamp":1751606375142,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:00:00Z","timestamp":1712880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-2104882","CNS-2107147"],"award-info":[{"award-number":["CNS-2104882","CNS-2107147"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSERC","award":["Discovery Grant"],"award-info":[{"award-number":["Discovery Grant"]}]},{"DOI":"10.13039\/501100012600","name":"ShanghaiTech University","doi-asserted-by":"publisher","award":["Startup Grant"],"award-info":[{"award-number":["Startup Grant"]}],"id":[{"id":"10.13039\/501100012600","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,12]]},"DOI":"10.1145\/3597503.3639203","type":"proceedings-article","created":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T16:43:26Z","timestamp":1712940206000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Declarative Smart Contracts"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8574-2120","authenticated-orcid":false,"given":"Haoxian","family":"Chen","sequence":"first","affiliation":[{"name":"ShanghaiTech University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6492-5221","authenticated-orcid":false,"given":"Lan","family":"Lu","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6583-9041","authenticated-orcid":false,"given":"Brendan","family":"Massey","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3370-2431","authenticated-orcid":false,"given":"Yuepeng","family":"Wang","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Burnaby, British Columbia, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4757-1746","authenticated-orcid":false,"given":"Boon Thau","family":"Loo","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,4,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/www.kingoftheether.com\/postmortem.html","author":"King","year":"2016","unstructured":"King of the ether throne --- post-mortem investigation. https:\/\/www.kingoftheether.com\/postmortem.html, 2016."},{"key":"e_1_3_2_1_2_1","volume-title":"https:\/\/www.coindesk.com\/learn\/2016\/06\/25\/understanding-the-dao-attack\/","author":"Understanding","year":"2016","unstructured":"Understanding the dao attack. https:\/\/www.coindesk.com\/learn\/2016\/06\/25\/understanding-the-dao-attack\/, 2016."},{"key":"e_1_3_2_1_3_1","volume-title":"https:\/\/blogs.360.net\/post\/Fairness_Analysis_of_Dice2win_EN.html","author":"Not","year":"2018","unstructured":"Not a fair game - fairness analysis of dice2win. https:\/\/blogs.360.net\/post\/Fairness_Analysis_of_Dice2win_EN.html, 2018."},{"key":"e_1_3_2_1_4_1","volume-title":"https:\/\/github.com\/ethereum\/solidity\/issues\/13073","author":"Cannot","year":"2022","unstructured":"Cannot replicate smtchecker example output. https:\/\/github.com\/ethereum\/solidity\/issues\/13073, 2022."},{"volume-title":"https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts","year":"2022","key":"e_1_3_2_1_5_1","unstructured":"Openzeppelin. https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts, 2022."},{"key":"e_1_3_2_1_6_1","volume-title":"https:\/\/docs.soliditylang.org\/en\/v0.8.17\/smtchecker.html","author":"Smtchecker","year":"2022","unstructured":"Smtchecker and formal verification. https:\/\/docs.soliditylang.org\/en\/v0.8.17\/smtchecker.html, 2022."},{"key":"e_1_3_2_1_7_1","volume-title":"https:\/\/docs.soliditylang.org\/en\/v0.8.17\/solidity-by-example.html","author":"Solidity","year":"2022","unstructured":"Solidity by example. https:\/\/docs.soliditylang.org\/en\/v0.8.17\/solidity-by-example.html, 2022."},{"key":"e_1_3_2_1_8_1","volume-title":"https:\/\/github.com\/ethereum\/solidity","author":"The","year":"2022","unstructured":"The solidity contract-oriented programming language. https:\/\/github.com\/ethereum\/solidity, 2022."},{"key":"e_1_3_2_1_9_1","volume-title":"https:\/\/github.com\/eth-sri\/verx-benchmarks","author":"Verx","year":"2022","unstructured":"Verx smart contract verification benchmarks. https:\/\/github.com\/eth-sri\/verx-benchmarks, 2022."},{"volume-title":"https:\/\/github.com\/Z3Prover\/z3","year":"2022","key":"e_1_3_2_1_10_1","unstructured":"Z3. https:\/\/github.com\/Z3Prover\/z3, 2022."},{"volume-title":"https:\/\/github.com\/ethereum\/act","year":"2023","key":"e_1_3_2_1_11_1","unstructured":"Act. https:\/\/github.com\/ethereum\/act, 2023."},{"volume-title":"https:\/\/etherscan.io\/tokens","year":"2023","key":"e_1_3_2_1_12_1","unstructured":"Erc-20 top tokens. https:\/\/etherscan.io\/tokens, 2023."},{"volume-title":"https:\/\/etherscan.io\/tokens-nft","year":"2023","key":"e_1_3_2_1_13_1","unstructured":"Non-fungible tokens (nft). https:\/\/etherscan.io\/tokens-nft, 2023."},{"volume-title":"https:\/\/github.com\/ConsenSys\/Scribble","year":"2023","key":"e_1_3_2_1_14_1","unstructured":"Scribble. https:\/\/github.com\/ConsenSys\/Scribble, 2023."},{"key":"e_1_3_2_1_15_1","volume-title":"https:\/\/github.com\/kupl\/VeriSmart-public\/commit\/858af814fbdab0c9d85b758e4c4575402ebf2bdf","author":"Verismart","year":"2023","unstructured":"Verismart commit on may 31, 2020. https:\/\/github.com\/kupl\/VeriSmart-public\/commit\/858af814fbdab0c9d85b758e4c4575402ebf2bdf, 2023."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549121"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2020.24449"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_30"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678888"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3559384"},{"key":"e_1_3_2_1_23_1","first-page":"2757","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Frank Joel","year":"2020","unstructured":"Joel Frank, Cornelius Aschermann, and Thorsten Holz. ETHBMC: A bounded model checker for smart contracts. In 29th USENIX Security Symposium (USENIX Security 20), pages 2757--2774. USENIX Association, August 2020."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_3_2_1_26_1","first-page":"161","volume-title":"Working conference on verified software: theories, tools, and experiments","author":"Hajdu \u00c1kos","year":"2019","unstructured":"\u00c1kos Hajdu and Dejan Jovanovi\u0107. solc-verify: A modular verifier for solidity smart contracts. In Working conference on verified software: theories, tools, and experiments, pages 161--179. Springer, 2019."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_18"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385982"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_12"},{"key":"e_1_3_2_1_33_1","first-page":"980","volume-title":"Model-checking of smart contracts. In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications","author":"Nehai Zeinab","year":"2018","unstructured":"Zeinab Nehai, Pierre-Yves Piriou, and Frederic Daumas. Model-checking of smart contracts. In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pages 980--987. IEEE, 2018."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59144-5_34"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_3_2_1_37_1","volume-title":"Sereum: Protecting existing smart contracts against re-entrancy attacks. arXiv preprint arXiv:1812.05934","author":"Rodler Michael","year":"2018","unstructured":"Michael Rodler, Wenting Li, Ghassan O Karame, and Lucas Davi. Sereum: Protecting existing smart contracts against re-entrancy attacks. arXiv preprint arXiv:1812.05934, 2018."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_3_2_1_40_1","first-page":"1361","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"So Sunbeom","year":"2021","unstructured":"Sunbeom So, Seongjoon Hong, and Hakjoo Oh. {SmarTest}: Effectively hunting vulnerable transaction sequences in smart contracts through language {Model-Guided} symbolic execution. In 30th USENIX Security Symposium (USENIX Security 21), pages 1361--1378, 2021."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00032"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510454.3516855"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00085"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2018.8500488"},{"key":"e_1_3_2_1_46_1","first-page":"87","volume-title":"Working Conference on Verified Software: Theories, Tools, and Experiments","author":"Wang Yuepeng","year":"2019","unstructured":"Yuepeng Wang, Shuvendu K Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, and Kostas Ferles. Formal verification of workflow policies for smart contracts in azure blockchain. In Working Conference on Verified Software: Theories, Tools, and Experiments, pages 87--106. Springer, 2019."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_21"}],"event":{"name":"ICSE '24: IEEE\/ACM 46th International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS","Faculty of Engineering of University of Porto"],"location":"Lisbon Portugal","acronym":"ICSE '24"},"container-title":["Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639203","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597503.3639203","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597503.3639203","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:13Z","timestamp":1750286953000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597503.3639203"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,12]]},"references-count":47,"alternative-id":["10.1145\/3597503.3639203","10.1145\/3597503"],"URL":"https:\/\/doi.org\/10.1145\/3597503.3639203","relation":{},"subject":[],"published":{"date-parts":[[2024,4,12]]},"assertion":[{"value":"2024-04-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}