All-Solution Satisfiability Modulo Theories: Applications, Algorithms and Benchmarks
All-Solution Satisfiability Modulo Theories: Applications, Algorithms and Benchmarks
复制标题
DOI：
10.1109/ares.2015.14
复制
发表时间：
2015-08
期刊：
影响因子：
--
通讯作者：
Quoc-Sang Phan;P. Malacaria
中科院分区：
文献类型：
--
作者：
Quoc-Sang Phan;P. Malacaria
可满足性模理论（SMT）是一个关于一个或多个一阶理论的逻辑公式的判定问题。在本文中，我们研究的问题，寻找所有解决方案的SMT问题的一组布尔变量，以下所有SMT。首先，我们展示了一个全SMT求解器如何使各种应用领域受益：有界模型检查，自动测试生成，可靠性分析和定量信息流。其次，我们提出了算法来设计一个全SMT求解器上现有的SMT求解器，并将其实现到一个原型工具，称为AZ 3。第三，我们在线性整数运算理论QF_LIA和带数组的位向量理论QF_AUFBV和未解释函数QF_AUFBV方面为All-SMT创建了一组基准测试。我们在我们的基准测试中将aZ 3与Math SAT（唯一现有的全SMT求解器）进行比较。实验结果表明，aZ 3比Math SAT更精确。
Satisfiability Modulo Theories (SMT) is a decision problem for logical formulas over one or more first-order theories. In this paper, we study the problem of finding all solutions of an SMT problem with respect to a set of Boolean variables, henceforth All-SMT. First, we show how an All-SMT solver can benefit various domains of application: Bounded Model Checking, Automated Test Generation, Reliability analysis, and Quantitative Information Flow. Secondly, we then propose algorithms to design an All-SMT solver on top of an existing SMT solver, and implement it into a prototype tool, called aZ3. Thirdly, we create a set of benchmarks for All-SMT in the theory of linear integer arithmetic QF_LIA and the theory of bit vectors with arrays and uninterpreted functions QF_AUFBV. We compare aZ3 against Math SAT, the only existing All-SMT solver, on our benchmarks. Experimental results show that aZ3 is more precise than Math SAT.