Hozzová, P., Bendík, J., Nutz, A., & Rodeh, Y. (2023). Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 257–269). EasyChair. https://doi.org/10.29007/h4p7
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
Volume:
94
-
Date (published):
3-Jun-2023
-
Event name:
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
en
Event date:
4-Jun-2023 - 9-Jun-2023
-
Event place:
Manizales, Colombia
-
Number of Pages:
13
-
Publisher:
EasyChair
-
Keywords:
formal verification; Linear Integer Arithmetic; non-linear integer arithmetic; non-linear real arithmetic; smart contracts; SMT solving
en
Abstract:
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.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Logische Komplexität und Termstruktur: P 35787-N (FWF - Österr. Wissenschaftsfonds) Doktoratskolleg: W 1255-N23 (FWF - Österr. Wissenschaftsfonds)
CC BY-NC-ND 4.0
