The ELDARICA Horn Solver
The ELDARICA Horn Solver
复制标题
ELDARICA 号角求解器
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
P. Rümmer
中科院分区：
文献类型：
--
作者：
Hossein Hojjat;P. Rümmer
本文介绍了ELDARICA第二版模型检验器。在过去的几年里，我们一直在开发和维护ELDARICA作为一个国家的最先进的解决方案霍恩子句在整数运算。在第2版中，我们扩展了求解器以支持代数数据类型和位向量，这些理论通常应用于验证，但目前大多数Horn求解器都不支持。本文介绍了该工具的高级结构和它提供给其他应用程序的接口。我们还报告了对该工具的评估。虽然在过去的几年中，ELDARICA中的一些技术已经在研究论文中被记录下来，但这是第一篇完整描述ELDARICA的工具论文。
This paper presents the ELDARICA version 2 model checker. Over the last years we have been developing and maintaining ELDARICA as a state-of-the-art solver for Horn clauses over integer arithmetic. In the version 2, we have extended the solver to support also algebraic data types and bit-vectors, theories that are commonly applied in verification, but currently unsupported by most Horn solvers. This paper describes the high-level structure of the tool and the interface that it provides to other applications. We also report on an evaluation of the tool. While some of the techniques in ELDARICA have been documented in research papers over the last years, this is the first tool paper describing ELDARICA in its entirety.