{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:58:45Z","timestamp":1782878325393,"version":"3.54.5"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2027977, 1908494, 1811865, 1762299"],"award-info":[{"award-number":["2027977, 1908494, 1811865, 1762299"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>As smart contracts gain adoption in financial transactions, it becomes increasingly important to ensure that they are free of bugs and security vulnerabilities. Of particular relevance in this context are arithmetic overflow bugs, as integers are often used to represent financial assets like account balances. Motivated by this observation, this paper presents SolType, a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in smart contracts. SolType allows developers to add refinement type annotations and uses them to prove that arithmetic operations do not lead to over- and under-flows. SolType incorporates a rich vocabulary of refinement terms that allow expressing relationships between integer values and aggregate properties of complex data structures. Furthermore, our implementation, called Solid, incorporates a type inference engine and can automatically infer useful type annotations, including non-trivial contract invariants.<\/jats:p>\n          <jats:p>To evaluate the usefulness of our type system, we use Solid to prove arithmetic safety of a total of 120 smart contracts. When used in its fully automated mode (i.e., using Solid's type inference capabilities), Solid is able to eliminate 86.3% of redundant runtime checks used to guard against overflows. We also compare Solid against a state-of-the-art arithmetic safety verifier called VeriSmart and show that Solid has a significantly lower false positive rate, while being significantly faster in terms of verification time.<\/jats:p>","DOI":"10.1145\/3498665","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["SolType: refinement types for arithmetic overflow in solidity"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4008-3846","authenticated-orcid":false,"given":"Bryan","family":"Tan","sequence":"first","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Mariano","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yu","family":"Feng","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_2_2_2_1","volume-title":"4th International Symposium, FMCO 2005","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett , Bor-Yuh Evan Chang , Robert DeLine , Bart Jacobs , and K. Rustan M. Leino . 2005 . Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects , 4th International Symposium, FMCO 2005 , Amsterdam, The Netherlands , November 1-4, 2005, Revised Lectures, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.) (Lecture Notes in Computer Science, Vol. 4111). Springer, 364\u2013387. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.) (Lecture Notes in Computer Science, Vol. 4111). Springer, 364\u2013387."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_7_1","unstructured":"2021. The Ethereum Blockchain Explorer. https:\/\/etherscan.io\/  2021. The Ethereum Blockchain Explorer. https:\/\/etherscan.io\/"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886663"},{"key":"e_1_2_2_15_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. The Internet Society. http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2018\/02\/ndss2018_09-1_Kalra_paper.pdf 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. The Internet Society. http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2018\/02\/ndss2018_09-1_Kalra_paper.pdf"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385982"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_20_1","unstructured":"Adriana M.. 2018. Real Estate Business Integrates Smart Contracts. https:\/\/coindoo.com\/real-estate-business-integrates-smart-contracts\/  Adriana M.. 2018. Real Estate Business Integrates Smart Contracts. https:\/\/coindoo.com\/real-estate-business-integrates-smart-contracts\/"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416626"},{"key":"e_1_2_2_22_1","unstructured":"Mix. 2018. Ethereum bug causes integer overflow in numerous ERC20 smart contracts (Update). https:\/\/thenextweb.com\/news\/ethereum-smart-contract-integer-overflow  Mix. 2018. Ethereum bug causes integer overflow in numerous ERC20 smart contracts (Update). https:\/\/thenextweb.com\/news\/ethereum-smart-contract-integer-overflow"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00133"},{"key":"e_1_2_2_24_1","unstructured":"2020. Mythril. https:\/\/github.com\/ConsenSys\/mythril  2020. Mythril. https:\/\/github.com\/ConsenSys\/mythril"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594318"},{"key":"e_1_2_2_26_1","unstructured":"Santiago Palladino. 2017. On the parity wallet multisig hack. https:\/\/blog.openzeppelin.com\/on-the-parity-wallet-multisig-hack-405a8c12e8f7\/  Santiago Palladino. 2017. On the parity wallet multisig hack. https:\/\/blog.openzeppelin.com\/on-the-parity-wallet-multisig-hack-405a8c12e8f7\/"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_32_1","unstructured":"David Siegel. 2016. Understanding The DAO Attack. https:\/\/www.coindesk.com\/learn\/2016\/06\/25\/understanding-the-dao-attack\/  David Siegel. 2016. Understanding The DAO Attack. https:\/\/www.coindesk.com\/learn\/2016\/06\/25\/understanding-the-dao-attack\/"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00032"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_2_2_36_1","unstructured":"Brian Straight. 2020. Smart contracts may offer smart solutions for carriers truck drivers. https:\/\/www.freightwaves.com\/news\/smart-contracts-may-offer-smart-solutions-for-carriers-truck-drivers  Brian Straight. 2020. Smart contracts may offer smart solutions for carriers truck drivers. https:\/\/www.freightwaves.com\/news\/smart-contracts-may-offer-smart-solutions-for-carriers-truck-drivers"},{"key":"e_1_2_2_37_1","unstructured":"Bryan Tan Benjamin Mariano Shuvendu K. Lahiri Isil Dillig and Yu Feng. 2021. SolType: extended version. arxiv:2110.00677.  Bryan Tan Benjamin Mariano Shuvendu K. Lahiri Isil Dillig and Yu Feng. 2021. SolType: extended version. arxiv:2110.00677."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498665","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498665","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498665"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498665"],"URL":"https:\/\/doi.org\/10.1145\/3498665","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}