有限域的 SMT-LIB 理论
计算机科学中的逻辑
2024-08-01 v1
摘要
过去几年来，针对有限域的 SMT 求解器开发迅猛。包括新的决策程序、对 SMT 理论求解器的新实现，以及依赖有限域 SMT 求解的新型软件验证器。为支持这一新兴生态系统的互操作性，我们提出了有限域算术 (FFA) 的 SMT-LIB 理论。该理论定义了有限域元素的规范表示，以及有限域元素上的操作和谓词。
引用
@article{arxiv.2407.21169,
title = {An SMT-LIB Theory of Finite Fields},
author = {Thomas Hader and Alex Ozdemir},
journal= {arXiv preprint arXiv:2407.21169},
year = {2024}
}