Z3: An efficient SMT solver

被引：4912
作者：
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 [J].
Ball, T ;
Rajamani, SK .
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 [J].
Detlefs, D ;
Nelson, G ;
Saxe, JB .
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