Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
我们提出了一个组合SMT为基础的算法的安全程序，考虑到堆以及。现有的基于SMT的方法要么在很大程度上限于处理线性算术运算和属性，或者是非组合的。我们使用约束角子句（CHCs）来表示验证条件，其中使用阵列的扩展理论（ARR）的内存操作建模。首先，我们描述了一个指数时间量词消去（QE）算法的ARR，它可以引入新的量词的索引和值排序。其次，我们适应QE算法，以有效地获得下近似使用模型，从而在多项式时间基于模型的投影（MBP）算法。第三，我们集成的MBP算法的框架中的组合推理的过程性程序使用的可能和必须的摘要，我们最近提出的。我们对CHC的解决方案目前仅限于无量词公式。最后，我们描述了我们的实践经验，在SV-COMP'15基准测试中使用的工具SPACER的实现。
2015-08-06 cs.LO cs.PL cs.SE
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
带抑制弧的参数时间Petri网（PITPN）允许参数在触发范围内，从而支持时间系统的灵活性。本文提出并证明了PITPN的一种具体的和符号化的重写逻辑语义。我们将展示如何使用Maude结合SMT解决方案，为PITPN提供完善的正式分析。我们开发了一个新的通用折叠符号可达性的方法，终止时的参数状态类图的PITPN是有限的。我们解释了几乎所有的形式分析和参数合成支持的国家的最先进的PITPN工具Roméo可以在Maude与SMT。此外，我们还支持从参数化初始标记进行分析和参数合成，以及使用用户定义的执行策略进行完整的LTL模型检验和分析。在三个基准上的实验表明，我们的方法在许多情况下优于Roméo。
2023-03-15 cs.LO
On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
众所周知，并发系统很难分析，而诸如弱内存架构之类的技术进步极大地加剧了这个问题。这重新引起了人们对偏序语义作为形式化验证技术的理论基础的兴趣。其中，符号技术已被证明是特别有效的发现并发相关的错误，因为它们可以利用高度优化的决策过程，如SAT/SMT求解器。本文给出了新的偏序语义SAT/SMT为基础的弱内存并发的符号编码的基本结果。特别是，我们给出了一个决策过程，可以处理并发程序的片段赋予最少不动点算子的理论基础。此外，我们表明，一定的偏序语义放松顺序一致性是等价的结合三个广泛研究的弱记忆公理Alglave等人。这种等价性的一个重要后果是一个渐进较小的符号编码有界模型检验只有一个平方数的偏序约束相比，国家的最先进的尺寸编码。
2015-03-31 cs.LO
SMT-based Symbolic Model-Checking for Operator Precedence Languages
针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。
2024-05-18 cs.LO
Can LLM Aid in Solving Constraints with Inductive Definitions?
本文提出一种神经符号方法，利用大语言模型生成辅助引理，提升求解涉及归纳定义的约束的能力，实验表明其在证明任务上的有效性。
2026-03-12 cs.AI cs.LO
An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis
本文实现并扩展一种高效典范窄化算法，使其支持带 SMT 条件约束的条件重写理论，从而增强通用符号密码协议分析能力。
2023-07-12 cs.LO cs.SC
Fast Approximations of Quantifier Elimination
针对精确量词消去计算成本高的问题，提出基于egraph数据结构的QEL框架，统一支持量化约简与基于模型的投影，实现了数组和ADT理论的MBP，集成到Z3后在相关任务中性能优于现有最优方法。
2023-06-16 cs.LO
Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis
Department of Management Information Systems, National ChengChi University, Taipei, Taiwan（管理信息系，中华大学，台北，台湾）；Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan（电子工程系，台湾大学，台北，台湾）
本研究整合大语言模型与SMT求解器，提出神经符号合规框架，用于自动化金融法律分析，实现形式可验证性和基于优化的合规修正。
2026-01-07 cs.AI cs.FL cs.LG
Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions
Cuvée是一个程序验证工具，它可以读取类似SMT-LIB的输入文件，其中的术语可能还包含抽象程序中最弱的前提运算符。Cuvée通过象征性地执行这些程序将这些输入转换为一阶SMT-LIB。Cuvée使用的输入格式旨在实现类似的工具统一，例如合成循环摘要。Cuvée本身的一个值得注意的技术方面是随后使用循环前/后条件，而不是不变式，我们演示了这是如何降低一些简单的while程序的注释负担。
2020-10-10 cs.LO
SMT-based Induction Methods for Timed Systems
在验证方法的许多应用中，对时间相关方面进行建模是很重要的。对于精确的结果，有必要将时间解释为密集域，例如使用时间自动机作为形式主义，即使系统产生的无限状态空间对验证方法具有挑战性。此外，完全符号化处理的状态空间的定时相关和非定时相关的元素似乎提供了一个有吸引力的方法，模型检验定时系统与大量的非确定性。本文提出了一种基于SMT的定时系统扩展的IC 3算法，一种新的，高效的，完整的验证方法，基于SAT的非定时系统。在扩展的IC 3算法中，对时间系统的无限状态空间的处理是基于对时间系统的区域抽象进行适当的调整。此外，$k$ -感应，另一个符号验证方法的离散时间系统，以类似的方式扩展到支持定时系统。这两种新的方法进行评估和实验比较，使用原来的离散时间IC 3算法的基于布尔化的验证方法。
2012-04-25 cs.LO
Delta-Decision Procedures for Exists-Forall Problems over the Reals
解决实数上的非线性SMT问题在机器人和人工智能中有着广泛的应用。虽然该领域在解决无量词SMT公式方面取得了重大进展，但量化公式的研究却少得多。我们提出了第一个Delta-完全算法，用于解决实数上的非线性SMT的可满足性，具有泛量化和广泛的非线性函数。我们的方法结合了反例指导的合成，间隔约束传播和局部优化的想法。特别是，我们展示了如何特别小心处理交织的数值和符号推理，以确保三角洲的完整性。在实验中，我们表明，所提出的算法可以处理许多新的问题超出了现有的SMT求解器。
2018-07-21 cs.LO
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
Bounded Structural Model Finding with Symbolic Data Constraints
University of Leicester（莱斯特大学）
本文提出Maude Model Finder，通过符号可达性实现结构求解，无需定制生成器，提供有限约束驱动的演算，支持对称性减少，并在声明范围内证明终止性、正确性和完备性。
2026-03-23 cs.LO
The VMT-LIB Language and Tools
我们提出了VMT-LIB，一种语言表示验证问题的线性时间的时间属性的无限状态符号转换系统。VMT-LIB是SMT求解器的标准SMT-LIB语言的扩展，其开发目标是促进不同验证工具之间的互操作性和基准问题的交换。除了描述它的语法和语义之外，我们还提供了一组使用该语言的开源工具。
2021-09-27 cs.LO
On Solving Quantified Bit-Vectors using Invertibility Conditions
提出了一种基于位向量算子符号逆运算的可满足性模理论（SMT）量化位向量公式求解方法。我们推导出的条件，精确地表征时，位向量的约束是可逆的一组代表性的位向量运算符通常支持SMT求解器。我们利用语法指导的合成技术来帮助建立这些条件，并通过使用几个SMT求解器独立验证它们。我们表明，可逆性条件可以嵌入到量词实例使用希尔伯特选择表达式，并给出实验证据，一个反例引导的方法，利用这些技术的量词实例化，导致性能改善相对于最先进的求解器量化的位向量约束。
2018-05-11 cs.LO
Transformation von Scade-Modellen zur SMT-basierten Verifikation
在这项工作中，我们开发了一个全自动的验证程序的安全性能的SCADE程序。我们将每个这样的程序转换为SMT实例（可满足性模理论），并将其提供给求解器。我们的目标是拥有一个可公开访问的实验平台，用于验证Scade程序。SMT的选择取决于它提供了比命题逻辑更多的表达逻辑，但它们的求解器已经被证明表现得非常好。SMT逻辑的表达能力使我们能够实现符号化的模型检验，从而避免了在验证过程中扩展模型的完整状态空间。为了降低复杂度，我们分两步将Scade程序转换为SMT实例。首先，它们被简化为同步数据流语言Lama的程序。这种语言的语义比Scade简单，同时仍然保留了一些程序员的抽象。接下来，我们解释这样一个喇嘛程序作为一个系统的量词自由的一阶公式。Lama中剩下的抽象可以用来简化这些系统。这反过来又可以加快核查进程，使更多的财产可以核查。我们使用Haskell在一个软件中成功地实现了这些转换。通过将该软件与Scade套件附带的现有验证软件“Scade Design Verifier”进行比较，得出了这项工作的结论。
2014-03-11 cs.LO
Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving
Florida International University（佛罗里达国际大学）；SRI International（SRI国际（斯坦福国际研究院））；United States Military Academy（美国军事学院（西点军校））；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Central Florida（中佛罗里达大学）；Vanderbilt University（范德堡大学）
本文提出 LLM 与 SMT 求解器迭代交互的神经符号框架，通过反例反馈修正规划综合结果，并在积木规划任务中验证其可生成可证明正确的解。
2023-09-28 cs.AI cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
symQV: Automated Symbolic Verification of Quantum Programs
我们提出了symQV，一个符号执行框架，用于在量子线路模型中编写和验证量子计算。symQV可以自动验证量子程序是否符合一阶规范。我们正式介绍了一个符号量子程序模型。这允许在SMT公式中编码验证问题，然后可以使用delta-完全决策过程进行检查。我们还提出了一个抽象技术，以加快验证过程。实验结果表明，该抽象将symQV的可扩展性提高了一个数量级，可以扩展到具有24个量子比特（2^24维状态空间）的量子程序。
2022-12-05 cs.LO quant-ph
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
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4
Xi’an Jiaotong-Liverpool University（西交利物浦大学）
提出ViaLean，通过持久证明状态图的受限探索组织符号推理，在miniF2F上无模型配置达到50.0% pass@1，并支持神经-符号智能体接口。
2026-10-06 cs.LO
A CDCL-style calculus for solving non-linear constraints
在本文中，我们提出了一种新的方法来检查实数上的非线性约束的可满足性，称为ksmt。该程序是基于CDCL风格的演算冲突解决，使用符号和数值方法的组合。为了处理冲突情况下的非线性组件，我们使用数字构造的限制线性化。这种方法涵盖了大量的可计算的非线性实函数，如多项式，有理或三角函数和超越。几个非线性SMT-LIB的例子和结果进行了比较，与国家的最先进的SMT求解器的原型实现进行了评估。
2019-07-05 cs.LO
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Shanghai Jiao Tong University（上海交通大学）
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
2026-09-30 cs.LO cs.PL cs.SE
Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
无限状态系统的安全性可以通过一个向后可达过程来检验。对于某些类型的系统，可以证明过程的终止，从而得出安全问题的可判定性。虽然向后可达性是属性导向的，但它可以不必要地探索系统的状态空间的（大）部分，这些部分不需要验证所考虑的安全属性。为了避免这种情况，可以使用不变量来大幅修剪搜索空间。事实上，问题是要猜测这样合适的不变量。在本文中，我们提出了一个完全声明性和符号化的方法来机械化的向后可达的无限状态系统操纵数组的可满足性模理论解决。理论用于指定拓扑结构和由系统操作的数据。我们确定的理论，以确保向后可达性的终止的充分条件，我们显示的完整性不变的合成方法（作为对偶的向后可达性），再次，在适当的假设下的理论。我们还提出了一个务实的方法交错不变的合成和向后可达性，使一组向后可达状态的不动点更容易获得。最后，我们讨论了算法，使我们能够得到一个实现的技术在模型检查MCMT，显示显着的速度加快了一组重要的安全问题，从各种来源提取。
2010-12-21 cs.LO
On Verifying Complex Properties using Symbolic Shape Analysis
软件系统验证的主要挑战之一是分析具有动态存储器分配的无界数据结构，例如链接数据结构和数组。我们描述Bohne，一个新的分析验证数据结构。Bohne验证了数据结构操作，并表明：1）操作保持数据结构不变，2）操作满足它们的规范，这些规范是根据存储在数据结构中的对象集的变化来表达的。在分析过程中，Bohne以普遍量化的布尔公式组合的析取形式推断循环不变量。为了合成这种形式的循环不变量，Bohne使用了树上一元二阶逻辑的决策过程，SMT-LIB决策过程（目前为CVC Lite）和Isabelle交互式定理证明器中的自动推理器的组合。这种架构表明，合成循环不变式可以作为一个有用的通信机制之间的不同的决策过程。使用Bohne，我们已经验证了数据结构上的操作，例如具有迭代器和反向指针的链表，具有和不具有父指针的树，两级跳表，数组数据结构和排序列表。我们已经在Hob和Jahob数据结构分析系统中部署了Bohne，使我们能够将Bohne与数据结构客户端的分析相结合，并将其应用于更大的程序。本报告描述了Bohne算法以及Bohne用于减少注释数量和分析运行时间的技术。
2006-09-18 cs.LO cs.PL cs.SE
Verifying Quantized Neural Networks using SMT-Based Model Checking
Federal University of Amazonas（亚马孙联邦大学）；University of Manchester（曼彻斯特大学）；TPV Technology（TPV技术公司）
人工神经网络（ANN）正被部署用于越来越多的安全关键型应用，包括自动驾驶汽车和医疗诊断。然而，由于其黑箱性质和对对抗攻击的明显脆弱性，人们对它们的可靠性提出了担忧。当人工神经网络部署在受限系统上时，这些问题被放大，这限制了数学运算的精度，从而引入了额外的量化误差。在这里，我们开发和评估一种新的符号验证框架，使用软件模型检验（SMC）和可满足性模理论（SMT）检查人工神经网络中的漏洞。更具体地说，我们提出了几个人工神经网络相关的优化SMC，包括通过区间分析，切片不变的推理，表达式简化，和离散化的非线性激活函数。有了这个验证框架，我们可以提供正式保证的安全行为的人工神经网络实现在浮点和定点运算。在这方面，我们的验证方法能够验证和产生对抗的例子，$52$测试用例跨越图像分类和一般的机器学习应用。此外，对于中小型ANN，我们的方法在几分钟内完成了大部分验证运行。此外，与大多数最先进的方法相比，我们的方法不限于关于激活函数和非量化表示的特定选择。我们的实验表明，我们的方法可以分析更大的ANN实现，并大大减少了验证时间相比，使用SMT解决的最先进的技术。
2021-09-16 cs.CR cs.LG cs.LO
Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所计算机科学国家重点实验室）；University of Chinese Academy of Sciences（中国科学院大学）；National University of Defense Technology（国防科技大学）；University of Liverpool（利物浦大学）；Institute of Intelligent Software, Guangzhou（广州智能软件研究院）
深度神经网络（DNN）已经被证明缺乏鲁棒性，因为它们的分类容易受到输入上的小扰动的影响。这导致了将DNN应用于安全关键域的安全问题。已经开发了几种验证方法来自动证明或反驳DNN的安全属性。然而，这些方法遭受可扩展性问题，即，只能处理小的DNN，或者精度问题，即，得到的边界是松散的。本文改进了最近提出的分析DNN通过经典的抽象解释技术，通过一种新的符号传播技术。更具体地说，神经元的值被符号化地表示，并在抽象域之上从输入层向前传播到输出层。我们表明，我们的方法可以实现显着更高的精度，从而可以证明更多的属性比只使用抽象域。此外，我们表明，来自我们的方法对隐藏的神经元的界限，当应用到一个国家的最先进的SMT基于验证工具，可以提高其性能。我们将我们的方法实现到一个软件工具中，并在一些在MNIST等基准数据集上训练的DNN上对其进行验证。
2021-02-23 cs.LG cs.LO
Synthesizing Composite Hierarchical Structure from Symbolic Music Corpora
University of California, San Diego, CA, USA（加州大学圣迭戈分校）；AudioShake, Oakland, CA, USA（AudioShake）
本文提出结构时间图（STG）统一表示音乐层次结构，通过模拟退火与SMT求解器结合，解决广义中值图问题，生成语料库代表性质心STG，实验验证了结构距离的区分性和质心的表征准确性。
2025-06-20 cs.AI cs.LO cs.SD
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Federal University of Amazonas（亚马逊联邦大学）；SIDIA Instituto de Ciência e Tecnologia（SIDIA科学技术研究所）；University of Manchester（曼彻斯特大学）
人工神经网络（ANN）是用于各种应用的强大的计算系统，这是由于其通用性来概括和响应意外的输入/模式。然而，人工神经网络的安全关键系统的实现可能会导致故障，这是很难预测的设计阶段，因为人工神经网络是高度并行的，他们的参数是很难解释。在这里，我们开发并评估了一种基于增量有界模型检验（BMC）的新型符号软件验证框架，以检查多层感知器（MLP）中的对抗性情况和覆盖方法。特别是，我们进一步开发了高效的基于SMT的图形处理单元上下文有界模型（ESBMC-GPU），以确保某些安全属性的可靠性，其中安全关键系统可能会出现故障并做出错误的决策，从而导致不必要的材料损坏甚至危及生命。本文标志着第一个符号验证框架的原因在CUDA实现的人工神经网络。我们的实验结果表明，我们在ESBMC-GPU上实现的方法可以成功地验证人工神经网络的安全属性和覆盖方法，并正确地生成28个MLP对抗案例。
2019-07-30 cs.LG cs.LO cs.NE
