{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,20]],"date-time":"2024-08-20T13:08:36Z","timestamp":1724159316716},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.<\/jats:p>","DOI":"10.29007\/h4p7","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:10Z","timestamp":1685830210000},"source":"Crossref","is-referenced-by-count":1,"title":["Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification"],"prefix":"10.29007","author":[{"given":"Petra","family":"Hozzov\u00e1","sequence":"first","affiliation":[]},{"given":"Jaroslav","family":"Bend\u00edk","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Nutz","sequence":"additional","affiliation":[]},{"given":"Yoav","family":"Rodeh","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:18Z","timestamp":1685830218000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/BlrQ"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/h4p7","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}