“Satisfiability Modulo Finite Fields” by Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett. In Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), (Constantin Enea and Akash Lal, eds.), July 2023, pp. 163-186. Paris, France.
We study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we construct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evaluate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors).
BibTeX entry:
@inproceedings{OKT+23,
author = {Alex Ozdemir and Gereon Kremer and Cesare Tinelli and Clark
Barrett},
editor = {Constantin Enea and Akash Lal},
title = {Satisfiability Modulo Finite Fields},
booktitle = {Proceedings of the {\it 35^{th}} International Conference
on Computer Aided Verification (CAV '23)},
series = {Lecture Notes in Computer Science},
volume = {13965},
pages = {163--186},
publisher = {Springer},
month = jul,
year = {2023},
doi = {10.1007/978-3-031-37703-7_8},
note = {Paris, France},
url = {https://link.springer.com/chapter/10.1007/978-3-031-37703-7_8}
}
(This webpage was created with bibtex2web.)