{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T09:11:23Z","timestamp":1780391483553,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T00:00:00Z","timestamp":1667779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001321","name":"National Research Foundation","doi-asserted-by":"publisher","award":["NRF2018NCR-NSOE004-0001"],"award-info":[{"award-number":["NRF2018NCR-NSOE004-0001"]}],"id":[{"id":"10.13039\/501100001321","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,11,7]]},"DOI":"10.1145\/3540250.3558923","type":"proceedings-article","created":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T20:46:22Z","timestamp":1668026782000},"page":"1687-1691","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["SolSEE: a source-level symbolic execution engine for solidity"],"prefix":"10.1145","author":[{"given":"Shang-Wei","family":"Lin","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Palina","family":"Tolmach","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore \/ IHPC at A*STAR, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ye","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,11,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/solidity.readthedocs.io\/en\/v0.5.11\/ Accessed","author":"Solidity","year":"2022","unstructured":"2020. Solidity \u2014 Solidity 0.5.11 documentation. https:\/\/solidity.readthedocs.io\/en\/v0.5.11\/ Accessed : June 19, 2022 2020. Solidity \u2014 Solidity 0.5.11 documentation. https:\/\/solidity.readthedocs.io\/en\/v0.5.11\/ Accessed: June 19, 2022"},{"key":"e_1_3_2_1_2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"Alt Leonardo","unstructured":"Leonardo Alt and Christian Reitwiessner . 2018. SMT-Based Verification of Solidity Smart Contracts . In Leveraging Applications of Formal Methods, Verification and Validation . Industrial Practice, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing , Cham . 376\u2013388. isbn:978-3-030-03427-6 Leonardo Alt and Christian Reitwiessner. 2018. SMT-Based Verification of Solidity Smart Contracts. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham. 376\u2013388. isbn:978-3-030-03427-6"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_1_4_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems . Springer Berlin Heidelberg , Berlin, Heidelberg . 337\u2013340. isbn:978-3-540-78800-3 Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg. 337\u2013340. isbn:978-3-540-78800-3"},{"key":"e_1_3_2_1_5_1","volume-title":"SMTChecker and Formal Verification. https:\/\/docs.soliditylang.org\/en\/latest\/smtchecker.html Accessed","year":"2022","unstructured":"Ethereum. 2022. SMTChecker and Formal Verification. https:\/\/docs.soliditylang.org\/en\/latest\/smtchecker.html Accessed : June 19, 2022 Ethereum. 2022. SMTChecker and Formal Verification. https:\/\/docs.soliditylang.org\/en\/latest\/smtchecker.html Accessed: June 19, 2022"},{"key":"e_1_3_2_1_6_1","volume-title":"Solidity in Depth \u2014 Solidity 0.5.11 Documentation. https:\/\/docs.soliditylang.org\/en\/v0.5.11\/solidity-in-depth.html Accessed","year":"2022","unstructured":"Ethereum. 2022. Solidity in Depth \u2014 Solidity 0.5.11 Documentation. https:\/\/docs.soliditylang.org\/en\/v0.5.11\/solidity-in-depth.html Accessed : June 19, 2022 Ethereum. 2022. Solidity in Depth \u2014 Solidity 0.5.11 Documentation. https:\/\/docs.soliditylang.org\/en\/v0.5.11\/solidity-in-depth.html Accessed: June 19, 2022"},{"key":"e_1_3_2_1_7_1","volume-title":"solc-verify: A Modular Verifier for Solidity Smart Contracts. CoRR, abs\/1907.04262","author":"Hajdu \u00c1kos","year":"2019","unstructured":"\u00c1kos Hajdu and Dejan Jovanovi\u0107 . 2019. solc-verify: A Modular Verifier for Solidity Smart Contracts. CoRR, abs\/1907.04262 ( 2019 ), arxiv:1907.04262. arxiv:1907.04262 \u00c1kos Hajdu and Dejan Jovanovi\u0107. 2019. solc-verify: A Modular Verifier for Solidity Smart Contracts. CoRR, abs\/1907.04262 (2019), arxiv:1907.04262. arxiv:1907.04262"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00066"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3141396"},{"key":"e_1_3_2_1_10_1","volume-title":"Source code of VeriSmart. https:\/\/github.com\/kupl\/VeriSmart-public\/ Accessed","year":"2022","unstructured":"kupl. 2022. Source code of VeriSmart. https:\/\/github.com\/kupl\/VeriSmart-public\/ Accessed : June 19, 2022 kupl. 2022. Source code of VeriSmart. https:\/\/github.com\/kupl\/VeriSmart-public\/ Accessed: June 19, 2022"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115689"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115690"},{"key":"e_1_3_2_1_13_1","volume-title":"SolSEE: Online Supplementary Material. https:\/\/sites.google.com\/view\/solsee\/ Accessed","author":"Lin Shang-Wei","year":"2022","unstructured":"Shang-Wei Lin , Palina Tolmach , Ye Liu , and Yi Li. 2022. SolSEE: Online Supplementary Material. https:\/\/sites.google.com\/view\/solsee\/ Accessed : May 26, 2022 Shang-Wei Lin, Palina Tolmach, Ye Liu, and Yi Li. 2022. SolSEE: Online Supplementary Material. https:\/\/sites.google.com\/view\/solsee\/ Accessed: May 26, 2022"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_15_1","volume-title":"Source code of VeriSol \u2014 A formal verifier and analysis tool for Solidity Smart Contracts. https:\/\/github.com\/microsoft\/verisol Accessed","year":"2022","unstructured":"Microsoft. 2022. Source code of VeriSol \u2014 A formal verifier and analysis tool for Solidity Smart Contracts. https:\/\/github.com\/microsoft\/verisol Accessed : June 19, 2022 Microsoft. 2022. Source code of VeriSol \u2014 A formal verifier and analysis tool for Solidity Smart Contracts. https:\/\/github.com\/microsoft\/verisol Accessed: June 19, 2022"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00133"},{"key":"e_1_3_2_1_17_1","unstructured":"Bernhard Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit. \t\t\t\t  Bernhard Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_19_1","volume-title":"DeFi - The Decentralized Finance Leaderboard at DeFi Pulse. https:\/\/defipulse.com\/ Accessed","author":"Pulse DeFi","year":"2022","unstructured":"DeFi Pulse . 2022. DeFi - The Decentralized Finance Leaderboard at DeFi Pulse. https:\/\/defipulse.com\/ Accessed : May 26, 2022 DeFi Pulse. 2022. DeFi - The Decentralized Finance Leaderboard at DeFi Pulse. https:\/\/defipulse.com\/ Accessed: May 26, 2022"},{"key":"e_1_3_2_1_20_1","volume-title":"React - A JavaScript library for building user interfaces. https:\/\/reactjs.org\/ Accessed","author":"Js.","year":"2022","unstructured":"React Js. 2022. React - A JavaScript library for building user interfaces. https:\/\/reactjs.org\/ Accessed : June 19, 2022 ReactJs. 2022. React - A JavaScript library for building user interfaces. https:\/\/reactjs.org\/ Accessed: June 19, 2022"},{"key":"e_1_3_2_1_21_1","volume-title":"https:\/\/github.com\/ethereum\/remix-project Accessed","author":"Remix","year":"2022","unstructured":"Remix. 2022. Remix IDE. https:\/\/github.com\/ethereum\/remix-project Accessed : June 19, 2022 Remix. 2022. Remix IDE. https:\/\/github.com\/ethereum\/remix-project Accessed: June 19, 2022"},{"key":"e_1_3_2_1_22_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"So Sunbeom","year":"2021","unstructured":"Sunbeom So , Seongjoon Hong , and Hakjoo Oh . 2021 . SmarTest: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution . In 30th USENIX Security Symposium (USENIX Security 21) . USENIX Association, 1361\u20131378. isbn:978-1-939133-24-3 https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/so Sunbeom So, Seongjoon Hong, and Hakjoo Oh. 2021. SmarTest: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1361\u20131378. isbn:978-1-939133-24-3 https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/so"},{"key":"#cr-split#-e_1_3_2_1_23_1.1","unstructured":"Sunbeom So Myungho Lee Jisu Park Heejo Lee and Hakjoo Oh. 2019. VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts. https:\/\/doi.org\/10.48550\/ARXIV.1908.11227 10.48550\/ARXIV.1908.11227"},{"key":"#cr-split#-e_1_3_2_1_23_1.2","unstructured":"Sunbeom So Myungho Lee Jisu Park Heejo Lee and Hakjoo Oh. 2019. VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts. https:\/\/doi.org\/10.48550\/ARXIV.1908.11227"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion55297.2022.9793786"},{"key":"e_1_3_2_1_25_1","volume-title":"Source Code of solc-verify\u2014a modular verifier for Solidity.. https:\/\/github.com\/SRI-CSL\/solidity\/tree\/boogie\/ Accessed","author":"SRI-CSL.","year":"2022","unstructured":"SRI-CSL. 2022. Source Code of solc-verify\u2014a modular verifier for Solidity.. https:\/\/github.com\/SRI-CSL\/solidity\/tree\/boogie\/ Accessed : June 19, 2022 SRI-CSL. 2022. Source Code of solc-verify\u2014a modular verifier for Solidity.. https:\/\/github.com\/SRI-CSL\/solidity\/tree\/boogie\/ Accessed: June 19, 2022"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp40001.2021.00085"},{"key":"e_1_3_2_1_27_1","volume-title":"Formal Analysis of Composable DeFi Protocols. In Financial Cryptography and Data Security. FC 2021 International Workshops. Springer Berlin Heidelberg","author":"Tolmach Palina","year":"2021","unstructured":"Palina Tolmach , Yi Li , Shang-Wei Lin , and Yang Liu . 2021 . Formal Analysis of Composable DeFi Protocols. In Financial Cryptography and Data Security. FC 2021 International Workshops. Springer Berlin Heidelberg , Berlin, Heidelberg. 149\u2013161. isbn:978-3-662-63958-0 Palina Tolmach, Yi Li, Shang-Wei Lin, and Yang Liu. 2021. Formal Analysis of Composable DeFi Protocols. In Financial Cryptography and Data Security. FC 2021 International Workshops. Springer Berlin Heidelberg, Berlin, Heidelberg. 149\u2013161. isbn:978-3-662-63958-0"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464421"},{"key":"e_1_3_2_1_29_1","volume-title":"Source code of VeriSol used in SmartPulse. https:\/\/github.com\/utopia-group\/verisol Accessed","year":"2022","unstructured":"utopia group. 2022. Source code of VeriSol used in SmartPulse. https:\/\/github.com\/utopia-group\/verisol Accessed : June 19, 2022 utopia group. 2022. Source code of VeriSol used in SmartPulse. https:\/\/github.com\/utopia-group\/verisol Accessed: June 19, 2022"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Yuepeng Wang Shuvendu Lahiri Shuo Chen Rong Pan Isil Dillig Cody Born and Immad Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. April https:\/\/www.microsoft.com\/en-us\/research\/publication\/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain\/ \t\t\t\t  Yuepeng Wang Shuvendu Lahiri Shuo Chen Rong Pan Isil Dillig Cody Born and Immad Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. April https:\/\/www.microsoft.com\/en-us\/research\/publication\/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain\/","DOI":"10.1007\/978-3-030-41600-3_7"}],"event":{"name":"ESEC\/FSE '22: 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Singapore Singapore","acronym":"ESEC\/FSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","NUS NUS"]},"container-title":["Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3540250.3558923","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3540250.3558923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:03Z","timestamp":1750182543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3540250.3558923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,7]]},"references-count":31,"alternative-id":["10.1145\/3540250.3558923","10.1145\/3540250"],"URL":"https:\/\/doi.org\/10.1145\/3540250.3558923","relation":{},"subject":[],"published":{"date-parts":[[2022,11,7]]},"assertion":[{"value":"2022-11-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}