The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk)
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk)
复制标题
SMT-LIB 计划和 SMT 的兴起 -（HVC 2010 颁奖演讲）
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
C. Tinelli
中科院分区：
文献类型：
--
作者：
Clark W. Barrett;L. D. Moura;Silvio Ranise;Aaron Stump;C. Tinelli
可满足性模理论（SMT）是自动推理的一个分支，它建立在命题可满足性和一阶推理决策过程的基础上。它的定义特征是在目标应用程序中使用特定于感兴趣的逻辑理论的推理方法。在SMT研究和技术的进步，导致在过去几年中非常强大的可满足性求解器的发展和爆炸式的应用。SMT求解器现在用于处理器验证、等价性检查、有界和无界模型检查、谓词抽象、静态分析、自动测试用例生成、扩展静态检查、调度和优化。虽然SMT的根源可以追溯到20世纪70年代末和80年代初在正式方法中使用决策过程的工作，但该领域诞生于20世纪90年代末，各种独立的尝试利用现代SAT求解器的力量，随着过去十年的研究和开发进展，达到了目前的复杂程度。这些进步的主要推动力是SMT-LIB，这是一个标准化和基准收集倡议，得到了世界各地大量SMT研究人员和用户的支持，它的后代：SMT研讨会，一个汇集SMT研究人员和SMT应用或技术用户的国际研讨会; SMT-COMP，一个支持SMT-LIB输入格式的SMT求解器的国际竞赛; SMT-EXEC是一个公共执行服务，允许研究人员在SMT求解器上配置和执行基准测试实验。
Satisfiability modulo theories (SMT) is a branch of automated reasoning that builds on advances in propositional satisfiability and on decision procedures for first-order reasoning. Its defining feature is the use of reasoning methods specific to logical theories of interest in target applications. Advances in SMT research and technology have led in the last few years to the development of very powerful satisfiability solvers and to an explosion of applications. SMT solvers are now used for processor verification, equivalence checking, bounded and unbounded model checking, predicate abstraction, static analysis, automated test case generation, extended static checking, scheduling and optimization. While the roots of SMT go back to work in the late 1970s and early 1980s on using decision procedures in formal methods, the field was born in the late 1990s with various independent attempts to harness the power of modern SAT solvers, reaching the current level of sophistication with the research and development advances of the last decade. Major enablers for these advances were SMT-LIB, a standardization and benchmark collection initiative supported by a large number of SMT researchers and users world-wide, and its offsprings: the SMT workshop, an international workshop bringing together SMT researchers and users of SMT applications or techniques; SMT-COMP, an international competition for SMT solvers supporting the SMT-LIB input format; and SMT-EXEC, a public execution service allowing researchers to configure and execute benchmarking experiments on SMT solvers.