A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction
本文提出了一种有效的，结合制定两个广泛使用的抽象方法位级验证：基于反例的抽象（CBA）和基于证明的抽象（PBA）。与以前的工作不同，这种新方法被制定为一个单一的，增量SAT问题，交错CBA和PBA开发的抽象自下而上的方式。有人认为，新的方法是简单的概念和实现明智的比以前的方法。作为额外的奖励，PBA部分不需要证明日志，这允许使用更广泛的SAT求解器。
2010-08-11 cs.LO
Revisiting Incremental Linearization for Nonlinear Integer Arithmetic
Czech Technical University in Prague（布拉格捷克理工大学）
本文针对非线性整数算术SMT问题，提出改进的增量线性化公理集，基于Z3实现独立求解器，在SMT-LIB的NIA基准上整体性能与顶尖求解器相当，在多项式约束基准上表现更优。
2026-08-06 cs.LO
SMT-Based Model Checking of Industrial Simulink Models
嵌入式系统的开发需要对模型进行形式化的分析，例如使用MATLAB/Simulink描述的模型。然而，工业模型的日益复杂使得分析变得困难。提出了一种基于SMT求解器的Simulink模型模型检验方法。所提出的方法旨在（1）复杂模型的自动化，高效和可理解的验证，（2）模型的数值精确分析，以及（3）使用SMT求解器（我们使用Z3）演示Simulink模型的分析。它首先将目标模型编码为数学算术和位向量域中的谓词逻辑公式。我们将探讨如何对各种Simulink模块进行精确编码。然后，该方法使用基于k-归纳的算法来验证给定的不变性，该算法提取涉及目标块的子系统并增量地展开执行路径。在实验中，我们将所提出的方法和其他工具应用于一组模型和属性。我们的方法成功地验证了大多数属性，包括那些未验证的其他工具。
2022-06-07 cs.LO
Satisfiability Modulo Transcendental Functions via Incremental Linearization
在本文中，我们提出了一个抽象的细化方法，可满足性模超越函数的理论，如指数和三角函数。超越函数在抽象空间中被表示为不可解释的，这是根据有理数上的线性算术与不可解释函数的组合理论来描述的，并且通过上界和下界分段线性函数来递增地公理化。适当的数值技术被用来确保超越函数的抽象是健全的，即使在存在无理数。我们的实验评估基准验证和数学证明了我们的方法的潜力，表明它相比delta-satisfiability /区间传播和方法的基础上定理证明。
2018-01-26 cs.LO
Subtropical Satisfiability
无量化器非线性算法（QF_NRA）在可满足性模理论求解（SMT）的许多应用中出现。因此，SMT理论求解器中相应约束的有效推理是高度相关的。我们提出了一个新的不完整的，但有效的和终止的方法来识别可满足的实例。该方法是来自亚热带方法最近推出的符号计算的背景下，计算单个非常大的多元多项式的实零点。我们的方法需要作为输入的严格的多项式不等式，这代表了超过40%的QF_NRA节的SMT-LIB库的基准连接。该方法将多项式抽象为自然数上的指数向量，并标记相应系数的符号。然后，依次使用SMT来解决实数上的线性问题，以探索性地找到合适的点，这些点可以转换回原始问题的满意点。SMT-LIB系统的实验表明，我们的方法本身不是一个足够强大的决策过程，但一个有价值的启发式使用的技术组合。
2017-06-28 cs.LO
IC3 Modulo Theories via Implicit Predicate Abstraction
我们提出了一种新的方法来推广的IC3算法不变检查从有限状态到无限状态的过渡系统，表示在一些背景理论。该过程是基于IC3与隐式（谓词）抽象的紧密集成，隐式（谓词）抽象是一种表示抽象转换而不显式计算抽象系统的技术，并且相对于谓词的增加是增量的。在这种情况下，IC3只在抽象状态空间的布尔级别上操作，发现抽象谓词上的归纳子句。理论推理被限制在底层SMT求解器中，并在执行可满足性检查时透明地应用。当当前的抽象允许一个虚假的反例时，它通过发现和添加足够的新谓词集来改进。重要的是，这可以以完全增量的方式完成，而不会丢弃在前一次搜索中找到的子句。所提出的方法有两个关键优点。首先，与IC 3当前的SMT泛化不同，它允许处理广泛的背景理论，而不依赖于临时扩展，例如量词消去或特定于理论的从句泛化程序，这些程序可能并不总是可用的，而且可能效率低下。其次，与直接探索具体的转换系统相比，使用抽象可以显著提高性能，正如我们的实验所证明的那样。
2013-10-25 cs.LO cs.SE
On Deciding Local Theory Extensions via E-matching
可满足性模理论（SMT）求解器结合了通常出现在软件中的数据类型的理论的决策过程。这使它们成为自动化验证问题的重要工具。经常遇到的一个限制是验证问题通常无法在求解器原生支持的理论中完全表达。许多求解器允许将特定于应用的理论规范为量化的公理，但它们的处理在狭窄的特殊情况之外是不完整的。在这项工作中，我们将展示如何SMT求解器可以用来获得完整的决策程序的局部理论扩展，一类重要的理论，是使用有限的公理实例判定。我们提出了一种算法，使用E-匹配在搜索过程中逐步生成实例，显着减少了生成的实例的数量相比，渴望实例化策略。我们已经使用了两个SMT求解器来实现该算法，并进行了广泛的实验评估的基准来自验证条件堆操作程序。我们相信，我们的研究结果是感兴趣的SMT求解器的用户以及他们的开发人员。
2015-08-27 cs.LO
SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout
SMT-Layout首次将布尔变量编码层级关系引入约束布局，通过预处理与增量求解实现真实GUI布局在低算力设备上的毫秒级实时交互。
2024-11-19 cs.HC cs.LO
Bounded Model Checking of Multi-threaded Software using SMT solvers
从单核处理器到多核处理器的过渡使得多线程软件成为计算机辅助验证的一个重要课题。在这里，我们描述和评估的ESBMC模型检查器的扩展，以支持验证多线程软件共享的变量和锁使用有界模型检验（BMC）的基础上可满足性模理论（SMT）。我们描述了三种方法来模型检查多线程软件和我们的建模的同步原语的Pthread库。在惰性方法中，我们生成所有可能的交织，并分别对每个交织调用BMC过程，直到我们找到一个bug，或者系统地探索了所有交织。在时间表记录方法中，我们将所有可能的交织编码成一个单一的公式，然后利用SMT求解器的高速。在欠近似加宽方法中，我们通过从SMT求解器生成的不可满足性证明中提取状态变量和交织的数量来减少状态空间。在所有这三种方法中，我们都使用了部分降阶（POR）技术来减少交织的数量。实验表明，我们的方法可以分析更大的问题，并大大减少验证时间相比，国家的最先进的技术，结合经典的POR方法与符号算法和其他实现反例引导抽象细化技术。
2010-03-19 cs.LO cs.SE
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
用非线性实算术（NRA）检验设计（表示为转移系统）的模型检验不变性质是一个重要而又困难的问题。一方面，NRA是一个难以解决的理论，另一方面，大多数强大的模型检验技术缺乏对NRA的支持。在本文中，我们提出了一个反例引导的抽象细化（CEGAR）的方法，利用微分的线性化技术，使使用成熟和有效的模型检验算法的过渡系统的线性实数运算（LRA）与未解释的功能（EUF）。实证评估的结果证实了这种方法的有效性和潜力。
2018-01-26 cs.LO
Approximate Translation from Floating-Point to Real-Interval Arithmetic
浮点运算（FPA）是实数运算（RA）的一种机械表示，其中每个运算都用舍入的对应运算代替。通过使用支持FPA逻辑的SMT解算器可以验证各种数值属性。然而，与RA相比，求解过程的可扩展性仍然有限。在本文中，我们提出了一个决定程序FPA，利用RA解决的效率。该方法将FP数抽象为有理区间，将FPA表达式抽象为区间算术（IA）表达式;然后，使用现成的RA求解器（我们使用CVC 4和Z3）求解IA公式以检查FPA公式的可满足性。为了换取抽象所获得的效率，求解过程变得准完整;当可满足性受到可能的数值错误的影响时，我们允许输出未知数。此外，我们的IA是精心形式化处理特殊值NaN。我们实现了所提出的方法，并在实验中将其与四个现有的SMT求解器进行了比较。因此，我们确认，我们的求解器是有效的舍入模式参数化的情况下。
2021-12-06 cs.LO
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
针对MCSat求解非线性整数算术SMT问题时赋值选择影响性能的问题，提出融合局部搜索的引导框架，结合加速爬山与可行集跳转实现于Yices2，并在SMT-LIB基准上完成评估。
2025-07-23 cs.LO
EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability
Vanderbilt University（范德堡大学）；University of Southern California（南加州大学）
针对 SAT/SMT 教学交互工具不足的问题，本文提出 EduSAT，集成 DPLL、ROBDD 及五类 NP 完全问题抽象，经评估全部求解器达到 100% 正确率。
2023-08-15 cs.AI cs.FL cs.LO
Fast Approximations of Quantifier Elimination
针对精确量词消去计算成本高的问题，提出基于egraph数据结构的QEL框架，统一支持量化约简与基于模型的投影，实现了数组和ADT理论的MBP，集成到Z3后在相关任务中性能优于现有最优方法。
2023-06-16 cs.LO
Harnessing Incremental Answer Set Solving for Reasoning in Assumption-Based Argumentation
University of Helsinki（赫尔辛基大学）；Graz University of Technology（格拉茨工业大学）
基于假设的论证（ABA）是一种中心结构化的论证形式。如最近所示，答案集编程（ASP），使有效地解决NP难推理任务的ABA在实践中，特别是在普遍研究的逻辑编程片段的ABA。在这项工作中，我们利用最近的进展，在增量ASP解决开发有效的算法推理任务的逻辑编程片段ABA的多项式层次结构的第二个层次，包括怀疑推理下的首选语义以及优先推理，大概是很难。特别是，我们开发了非平凡的反例指导的抽象细化程序的基础上，增量ASP解决这些任务。我们还表明经验的程序是显着更有效的比以前提出的算法的任务。本文件正在考虑被TPLP接受。
2021-08-09 cs.AI cs.LO
A DPLL(T) Framework for Verifying Deep Neural Networks
George Mason University（乔治梅森大学）；University of Virginia（弗吉尼亚大学）
本文提出NeuralSAT验证方法，将SMT求解器中的DPLL(T)算法与基于抽象的演绎理论求解器及冲突子句学习相结合，在具有挑战性的DNN验证基准上展现出显著优势。
2024-01-19 cs.LG cs.LO cs.SE
Z3str3: A String Solver with Theory-aware Branching
我们提出了一个新的字符串SMT求解器，Z3str3，这是快于它的竞争对手Z3str2，Norn，CVC 4，S3和S3P在大多数三个工业强度的基准，即卡鲁扎，PISA和IBM AppScan。Z3str3支持字符串等式、长度函数上的线性算术和正则语言成员谓词。Z3str3效率背后的关键算法创新是一种我们称之为理论感知分支的技术，其中我们修改了Z3的分支启发式算法，以考虑理论文字的结构来计算分支活动。在传统的DPLL（T）结构中，理论文字的结构是隐藏的DPLL（T）SAT求解器，因为布尔抽象的输入理论公式。相比之下，本文提出的理论感知技术将理论文字的结构暴露给DPLL（T）SAT求解器的分支启发式，从而使其能够在搜索过程中做出比其他方式更明智的决策。因此，Z3str3比其竞争对手具有更好的性能。
2017-04-26 cs.LO
Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
本文扩展了位向量抽象验证框架，支持CSS码、高距离表面码及大规模GHZ电路，证明可靠性并验证622个突变体，显著提升量子电路验证的规模与效率。
2026-10-06 cs.ET cs.LO quant-ph
