An SMT-LIB Theory of Finite Fields
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914893843660800 |
|---|---|
| author | Hader, Thomas Ozdemir, Alex |
| author_facet | Hader, Thomas Ozdemir, Alex |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_21169 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An SMT-LIB Theory of Finite Fields Hader, Thomas Ozdemir, Alex Logic in Computer Science 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. |
| title | An SMT-LIB Theory of Finite Fields |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.21169 |