Z3: An efficient SMT solver

被引：4725
|
作者：
de Moura, Leonardo [1 ]
Bjorner, Nikolaj [1 ]
机构：
[1] Microsoft Res, Redmond, WA 98074 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS | 2008年 / 4963卷
关键词：
D O I：
10.1007/978-3-540-78800-3_24
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. D is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.
引用
收藏
页码：337 / 340
页数：4
相关论文
共 50 条
  • [21] Torsion of polygons in Z3
    Tesi, M. C.
    Janse van Rensburg, E. J.
    Orlandini, E.
    Whittington, S. G.
    Journal of Physics A: Mathematical and General, 30 (14):
  • [22] Arithmetic Solving in Z3
    Bjorner, Nikolaj
    Nachmanson, Lev
    COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 26 - 41
  • [23] Toward the Z3*-theorem
    Toborg, Imke
    Waldecker, Rebecca
    COMMUNICATIONS IN ALGEBRA, 2021, 49 (07) : 2851 - 2889
  • [24] New Z3 strings
    Kneipp, Marco A. C.
    Liebgott, Paulo J.
    PHYSICS LETTERS B, 2016, 763 : 186 - 189
  • [25] Platonic solids in Z3
    Ionascu, Eugen J.
    Markov, Andrei
    JOURNAL OF NUMBER THEORY, 2011, 131 (01) : 138 - 145
  • [26] Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping
    Behr, Nicolas
    Heckel, Reiko
    Saadat, Maryam Ghaffari
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (330): : 126 - 144
  • [27] 摩托罗拉Z3
    通信技术, 2007, (03) : 56 - 57
  • [28] ON THE STEINHAUS TILING PROBLEM FOR Z3
    Goldstein, Daniel
    Mauldin, R. Daniel
    QUARTERLY JOURNAL OF MATHEMATICS, 2014, 65 (02): : 339 - 347
  • [29] BMW Z3: Nice, but not perfect
    Anon
    Design News (Boston), 2002, 56 (24):
  • [30] Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
    Brummayer, Robert
    Biere, Armin
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2009, 5505 : 174 - 177
12345