Welcome to the resource topic for 2023/091
Title:
Satisfiability Modulo Finite Fields
Authors: Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett
Abstract: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 verify the correctness of various zero knowledge proof
compilers on various input programs. Our experiments show that our
implementation is vastly superior to previous approaches (which encode
field arithmetic using integers or bit-vectors).
ePrint: https://eprint.iacr.org/2023/091
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .