The MathSAT 4SMT Solver
The MathSAT 4SMT Solver
复制标题
MathSAT 4SMT 求解器
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
R. Sebastiani
中科院分区：
文献类型：
--
作者：
Roberto Bruttomesso;A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani
我们提出了Mathsat 4，这是一种最先进的SMT求解器。 MathSAT 4处理了几种有用的理论：（组合）平等和未解释的函数，差异逻辑，线性算术和比特矢量理论。它是针对正式验证的明确设计的，因此提供了扩展SMT在此环境中的适用性的功能。特别是：模型生成（用于反例重建），模型枚举（用于谓词抽象），增量接口（用于BMC）以及不满意的核心和Craig interpolants（用于抽象细化）的计算。
We present MathSAT 4 , a state-of-the-art SMT solver. MathSAT 4 handles several useful theories: (combinations of) equality and uninterpreted functions, difference logic, linear arithmetic, and the theory of bit-vectors. It was explicitly designed for being used in formal verification, and thus provides functionalities which extend the applicability of SMT in this setting. In particular: model generation (for counterexample reconstruction), model enumeration (for predicate abstraction), an incremental interface (for BMC), and computation of unsatisfiable cores and Craig interpolants (for abstraction refinement).