Satisfiability Modulo Finite Fields

Alex Ozdemir; Gereon Kremer; Cesare Tinelli; Clark Barrett

doi:10.1007/978-3-031-37703-7_8

Back

Book chapter

Open access

Satisfiability Modulo Finite Fields

Alex Ozdemir, Gereon Kremer, Cesare Tinelli and Clark Barrett

Computer Aided Verification

Lecture Notes in Computer Science, v. 13965, Springer Nature Switzerland

01/01/2023

DOI: 10.1007/978-3-031-37703-7_8

Files and links (1)

url

https://doi.org/10.1007/978-3-031-37703-7_8View

Published (Version of record) Open Access

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 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).

Details

Title: Subtitle: Satisfiability Modulo Finite Fields
Creators: Alex Ozdemir - Stanford University
Gereon Kremer - Stanford University
Cesare Tinelli - University of Iowa
Clark Barrett - Stanford University
Resource Type: Book chapter
Publication Details: Computer Aided Verification
Series: Lecture Notes in Computer Science; v. 13965
DOI: 10.1007/978-3-031-37703-7_8
Publisher: Springer Nature Switzerland
Language: English
Date published: 01/01/2023
Academic Unit: Computer Science
Record Identifier: 9984447960302771

Metrics

71 Record Views