An SMT-LIB Theory of Finite Fields

Hader, Thomas; Ozdemir, Alex

doi:10.34726/8461

Record link:

http://hdl.handle.net/20.500.12708/210203
https://doi.org/10.34726/8461

Title:

Citation:

Hader, T., & Ozdemir, A. (2024). An SMT-LIB Theory of Finite Fields. In Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada, July, 22-23, 2024. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada. CEUR-WS.org. https://doi.org/10.34726/8461

reposiTUm DOI:

10.34726/8461

CatalogPlus:

AC17422631

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Hader, Thomas
Ozdemir, Alex

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies

Published in:

Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada, July, 22-23, 2024

Volume:

3725

Date (published):

2024

Event name:

22nd International Workshop on Satisfiability Modulo Theories (SMT 2024)

Event date:

22-Jul-2024 - 23-Jul-2024

Event place:

Montreal, Canada

Number of Pages:

Publisher:

CEUR-WS.org

Peer reviewed:

Yes

Keywords:

SMT solving; SMT-LIB; finite fields

Abstract:

In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite fields. To support interoperability in this emerging ecosystem, we propose the SMT-LIB theory of finite field arithmetic (FFA). The theory defines a canonical representation of finite field elements as well as definitions of operations and predicates on finite field elements.

Project (external):

NSF

Project ID:

2110397

Research Areas:

Logic and Computation: 100%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%

License:

CC BY 4.0