Combined Satisfiability Modulo Parametric Theories

Combined Satisfiability Modulo Parametric Theories
复制标题

组合可满足性模参数理论

DOI：
--
复制
发表时间：
2007
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
通讯作者：
C. Tinelli
C. Tinelli
中科院分区：
--
文献类型：
--
作者：
S. Krstic;A. Goel;J. Grundy;C. Tinelli

文献摘要

被引文献

相似文献

我们提供了一个新的理论基础，设计全面的SMT求解器，在一个实际的方向推广。我们定义了最恰当地表达常见数据类型的“逻辑”的参数理论。我们的主要结果是一个组合定理的决策程序不相交的这种理论。几乎所有的深度嵌套的数据结构（数组的列表，数组的集合。. .），在核查工作中出现的。
We give a fresh theoretical foundation for designing comprehensive SMT solvers, generalizing in a practically motivated direction. We define parametric theories that most appropriately express the "logic" of common data types. Our main result is a combination theorem for decision procedures for disjoint theories of this kind. Virtually all of the deeply nested data structures (lists of arrays of sets of . . . ) that arise in verification work are covered.