Z3: An efficient SMT solver

被引：4735
作者：
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
相关论文
共 13 条
  • [1] The SLAM project: Debugging system software via static analysis
    Ball, T
    Rajamani, SK
    [J]. ACM SIGPLAN NOTICES, 2002, 37 (01) : 1 - 3
  • [2] BARNETT M, 2004, LNCS, V3362, P49, DOI [DOI 10.1007/978-3-540-30569-9_3, 10.1007/978-3-540-30569-9_3, 10.1007]
  • [3] COSTA M, 2005, SOSP, P133
  • [4] de Moura L., 2007, MSRTR2007140
  • [5] de Moura L, 2007, LECT NOTES ARTIF INT, V4603, P183
  • [6] DELINE R, 2005, TYPED PROCEDURAL LAN
  • [7] DEMOURA L, 2007, SMT 2007
  • [8] Simplify: A theorem prover for program checking
    Detlefs, D
    Nelson, G
    Saxe, JB
    [J]. JOURNAL OF THE ACM, 2005, 52 (03) : 365 - 473
  • [9] Dutertre B, 2006, LECT NOTES COMPUT SC, V4144, P81, DOI 10.1007/11817963_11
  • [10] GULAVANI BS, 2006, SIGSOFT FSE, P117
12