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 条
  • [1] Scala to the Power of Z3: Integrating SMT and Programming
    Koeksal, Ali Sinan
    Kuncak, Viktor
    Suter, Philippe
    AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 400 - 406
  • [2] Z3 and SMT in Industrial R&D
    Bjorner, Nikolaj
    FORMAL METHODS, 2018, 10951 : 675 - 678
  • [3] ON THE GENUS OF Z3 X Z3 X Z3
    BRIN, MG
    SQUIER, CC
    EUROPEAN JOURNAL OF COMBINATORICS, 1988, 9 (05) : 431 - 443
  • [4] Z3 x Z3 crossed products
    Matzri, Eliyahu
    JOURNAL OF ALGEBRA, 2014, 418 : 1 - 7
  • [5] An efficient SMT solver for string constraints
    Tianyi Liang
    Andrew Reynolds
    Nestan Tsiskaridze
    Cesare Tinelli
    Clark Barrett
    Morgan Deters
    Formal Methods in System Design, 2016, 48 : 206 - 234
  • [6] An efficient SMT solver for string constraints
    Liang, Tianyi
    Reynolds, Andrew
    Tsiskaridze, Nestan
    Tinelli, Cesare
    Barrett, Clark
    Deters, Morgan
    FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (03) : 206 - 234
  • [7] Z3 and (×Z3)3 symmetry protected topological paramagnets
    Hrant Topchyan
    Vasilii Iugov
    Mkhitar Mirumyan
    Shahane Khachatryan
    Tigran Hakobyan
    Tigran Sedrakyan
    Journal of High Energy Physics, 2023
  • [8] Analyzing toys models of Arabidopsis and Drosophila using Z3 SMT-LIB
    Rodriguez Vega, Martin
    INDEPENDENT COMPONENT ANALYSES, COMPRESSIVE SAMPLING, WAVELETS, NEURAL NET, BIOSYSTEMS, AND NANOENGINEERING XII, 2014, 9118
  • [9] 宝马Z3
    汽车维修, 2001, (05) : 36 - 36
  • [10] Free product Z3 * Z3 of rotations with rational entries
    Liu, GY
    Robertson, LC
    LINEAR ALGEBRA AND ITS APPLICATIONS, 2000, 307 (1-3) : 183 - 192
12345