| ||||
| ||||
![]() Title:Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification Conference:LPAR 2023 Tags:formal verification, linear integer arithmetic, non-linear integer arithmetic, non-linear real arithmetic, smart contracts and SMT solving Abstract: The need to solve non-linear arithmetic constraints presents a major obstacle for 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 use of the overapproximation methods leads to solving a significant number of new problems. Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification ![]() Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification | ||||
Copyright © 2002 – 2025 EasyChair |