Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
<|reference_start|>Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification: 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.<|reference_end|>
@article{hozzová2024overapproximation,
    title={Overapproximation of Non-Linear Integer Arithmetic for Smart Contract
  Verification},
    author={Petra Hozzov'a, Jaroslav Bend'ik, Alexander Nutz, Yoav Rodeh},
    journal={arXiv preprint arXiv:2402.10174},
    year={2024},
    doi={10.29007/h4p7},
    archivePrefix={arXiv},
    eprint={2402.10174},
    primaryClass={cs.LO}
}