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 条
  • [41] Knotted polygons with curvature in Z3
    Orlandini, E
    Tesi, MC
    JOURNAL OF PHYSICS A-MATHEMATICAL AND GENERAL, 1998, 31 (47): : 9441 - 9454
  • [42] The elliptic gamma function and SL(3, Z) x Z3
    Felder, G
    Varchenko, A
    ADVANCES IN MATHEMATICS, 2000, 156 (01) : 44 - 76
  • [43] The Barcelogic SMT solver
    Bofill, Miquel
    Nieuwenhuis, Robert
    Oliveras, Albert
    Rodriguez-Carbonell, Enric
    Rubio, Albert
    COMPUTER AIDED VERIFICATION, 2008, 5123 : 294 - +
  • [44] ON THE GENUS OF THE SEMIDIRECT PRODUCT OF Z9 BY Z3
    BRIN, MG
    RAUSCHENBERG, DE
    SQUIER, CC
    JOURNAL OF GRAPH THEORY, 1989, 13 (01) : 49 - 61
  • [45] Z3, THE 1ST MOVE
    HERSCHBERG, B
    VANDENHERIK, J
    ICCA JOURNAL, 1990, 13 (02): : 53 - 54
  • [46] Supercharging Plant Configurations Using Z3
    Bjorner, Nikolaj
    Levatich, Maxwell
    Lopes, Nuno P.
    Rybalchenko, Andrey
    Vuppalapati, Chandrasekar
    INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, 2021, 12735 : 1 - 25
  • [47] Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
    Jha, Susmit
    Limaye, Rhishikesh
    Seshia, Sanjit A.
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2009, 5643 : 668 - 674
  • [48] Edge Z3 parafermions in fermionic lattices
    Teixeira, Raphael L. R. C.
    Dias da Silva, Luis G. G., V
    PHYSICAL REVIEW B, 2022, 105 (19)
  • [49] Z3 scalar singlet dark matter
    Belanger, Genevieve
    Kannike, Kristjan
    Pukhov, Alexander
    Raidal, Martti
    JOURNAL OF COSMOLOGY AND ASTROPARTICLE PHYSICS, 2013, (01):
  • [50] Moto Z3 Play海外发布
    刘刚
    计算机与网络, 2018, 44 (13) : 27 - 27
12345