Z3: An efficient SMT solver

被引:4725
|
作者
de Moura, Leonardo [1 ]
Bjorner, Nikolaj [1 ]
机构
[1] Microsoft Res, Redmond, WA 98074 USA
关键词
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 条
  • [31] Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
    Katz, Guy
    Barrett, Clark
    Dill, David L.
    Julian, Kyle
    Kochenderfer, Mykel J.
    COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 : 97 - 117
  • [32] PUNCTURED INTERVALS TILE Z3
    Cambie, Stijn
    MATHEMATIKA, 2021, 67 (02) : 489 - 497
  • [33] A characterization of regular tetrahedra in Z3
    Ionascu, Eugen J.
    JOURNAL OF NUMBER THEORY, 2009, 129 (05) : 1066 - 1074
  • [34] Schur rings over Z x Z3
    Chen, Gang
    He, Jiawei
    COMMUNICATIONS IN ALGEBRA, 2021, 49 (10) : 4434 - 4446
  • [35] The Structure of Simple Sets in Z3
    S. I. Veselov
    A. Yu. Chirkov
    Automation and Remote Control, 2004, 65 : 396 - 400
  • [36] WHAT IS THE ANSWER TO Z3=1
    ECKMANN, JP
    RECHERCHE, 1983, 14 (141): : 260 - 262
  • [37] SU(3)L x (Z3 x Z3) GAUGE SYMMETRY AND TRI- BIMAXIMAL MIXING
    Hattori, Chuichiro
    Matsunaga, Mamoru
    Matsuoka, Takeo
    Nakanishi, Kenichi
    MODERN PHYSICS LETTERS A, 2010, 25 (35) : 2981 - 2989
  • [38] ENTANGLEMENT COMPLEXITY OF GRAPHS IN Z3
    SOTEROS, CE
    SUMNERS, DW
    WHITTINGTON, SG
    MATHEMATICAL PROCEEDINGS OF THE CAMBRIDGE PHILOSOPHICAL SOCIETY, 1992, 111 : 75 - 91
  • [39] ON THOMAE FORMULAS FOR Z3 CURVES
    Hattori, Ryohei
    KYUSHU JOURNAL OF MATHEMATICS, 2012, 66 (02) : 393 - 409
  • [40] 亏群同构于Z3~2×Z3的块代数的结构
    戴康顺
    杨胜
    温州大学学报(自然科学版), 2016, 37 (03) : 15 - 20