Revisiting Incremental Linearization for Nonlinear Integer Arithmetic
Czech Technical University in Prague（布拉格捷克理工大学）
本文针对非线性整数算术SMT问题，提出改进的增量线性化公理集，基于Z3实现独立求解器，在SMT-LIB的NIA基准上整体性能与顶尖求解器相当，在多项式约束基准上表现更优。
2026-08-06 cs.LO
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
尽管最近在自动程序验证方面取得了进展，但递归数据结构的推理仍然是验证工具及其后端（如SMT和CHC求解器）的挑战。为了解决这一问题，我们引入了符号自动机关系（SAR）的概念，它将符号自动机和自动关系结合起来，并继承了它们在布尔运算下的封闭性等优良性质。我们认为SAR的可满足性问题，并表明，它是不可判定的一般，但我们可以构建一个健全的（但不完整）和自动满足性检查减少CHC解决。讨论了该方法在数据结构上的SMT和CHC求解中的应用，并通过实验验证了该方法的有效性。
2021-08-17 cs.LO cs.PL
Equational Bit-Vector Solving via Strong Gröbner Bases
本文利用强Gröbner基刻画位向量模算术的代数性质，改进乘法逆元计算并解决量化等式性质中的不变式生成问题，实验证明其在时间和内存上优于现有SMT求解方法。
2024-02-26 cs.LO cs.PL
SMT Sampling via Model-Guided Approximation
本文研究了可满足性模理论（SMT）中的可满足公式域，特别是对这些公式的大量满意赋值的自动生成。尽管SMT在模型检验和形式化验证方面有着悠久而成功的历史，但这方面的研究相对较少。先前的工作是为布尔公式和涉及位向量、数组和未解释函数（QF_AUFBV）的无量词一阶公式生成这样的赋值或样本。我们提出了一种新的方法，是适合于理论T的整数算术和T与数组和未解释的功能。该方法涉及到减少一般的采样问题，从一组独立的间隔，这可以有效地完成一个简单的采样实例。这种减少是通过扩展一个单一的模型-种子-使用自上而下的传播约束沿原来的一阶公式。
2022-12-13 cs.LO
Efficient Volume Computation for SMT Formulas
提出ttc算法，通过将SMT实线性算术公式的解空间分解为重叠凸多胞体并集来计算可满足区域体积，性能显著优于现有方法。
2025-08-13 cs.LO
On Deciding Local Theory Extensions via E-matching
可满足性模理论（SMT）求解器结合了通常出现在软件中的数据类型的理论的决策过程。这使它们成为自动化验证问题的重要工具。经常遇到的一个限制是验证问题通常无法在求解器原生支持的理论中完全表达。许多求解器允许将特定于应用的理论规范为量化的公理，但它们的处理在狭窄的特殊情况之外是不完整的。在这项工作中，我们将展示如何SMT求解器可以用来获得完整的决策程序的局部理论扩展，一类重要的理论，是使用有限的公理实例判定。我们提出了一种算法，使用E-匹配在搜索过程中逐步生成实例，显着减少了生成的实例的数量相比，渴望实例化策略。我们已经使用了两个SMT求解器来实现该算法，并进行了广泛的实验评估的基准来自验证条件堆操作程序。我们相信，我们的研究结果是感兴趣的SMT求解器的用户以及他们的开发人员。
2015-08-27 cs.LO
SMT-based Model Checking for Recursive Programs
提出了一种基于SMT的递归程序安全性验证的符号模型检验算法。该算法是模块化的，并单独分析程序。与其他基于SMT的方法不同，它既保持了程序摘要的“过度近似”，也保持了程序摘要的“欠近似”。欠近似用于分析过程调用，而无需内联。过近似用于阻止不可行的反例和检测收敛到一个证明。我们表明，程序和属性的可判定理论，该算法是保证找到一个反例，如果存在的。然而，效率依赖于用于量词消去（QE）的预言。对于布尔程序，该算法是一个多项式决策过程，匹配最佳BDD算法的最坏情况的界限。对于线性算术（整数和有理数），我们通过“懒惰地”应用QE给出了算法的有效实例。我们使用现有的插值技术来过度近似QE，并引入“基于模型的投影”来欠近似QE。在SV-COMP基准测试上的实验结果表明，该算法在最新水平上有了显著的改进。
2014-05-25 cs.LO
A Survey of Satisfiability Modulo Theory
可满足性模理论（SMT）是检验一阶公式在线性整数或实数算术或其他理论上的可满足性。在这篇综述中，我们解释了命题可满足性和合取的决策过程的组合，称为DPLL（T），以及替代的“自然域”方法。我们还涵盖了量词，克雷格插值，多项式算术，以及SMT求解器如何用于自动软件分析。
2016-06-15 cs.LO
Approximate Counting in SMT and Value Estimation for Probabilistic Programs
Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）
#SMT，或逻辑理论的模型计数，是一个众所周知的难题，它概括了诸如计算布尔公式的满意赋值的数量和计算多面体的体积等任务。在可满足性模理论（SMT）领域中，对来自若干应用领域（定量信息流、概率程序的静态分析）的模型计数求解器的需求日益增长。在本文中，我们展示了从#SMT到SMT的近似版本的减少。重点介绍了整数算术和线性实数算术的理论。我们提出了模型计数算法，提供近似解的近似误差的正式界限。它们在多项式时间内运行，并对SMT求解器进行多项式数量的查询以获得基础理论，从而“免费”利用现代SMT求解器内实现的复杂的几何学。我们已经实现了算法，并使用它们来解决一个模型的无循环概率程序的不确定性的值问题。
2015-10-29 cs.AI cs.LO
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
一元可分解性是变量独立性的概念，它询问一阶理论中的给定公式是否可以表示为理论中一元谓词的布尔组合。最近，Veanes等人在SMT的上下文中展示了一元可分解性的有用性（即输入公式是无量词的），并发现了各种有趣的应用，包括字符串分析。然而，检查一元可分解性通常是不可判定的。某些理论的可判定性是已知的（例如，Presburger算术，Tarski的实闭域），但关于它们的计算复杂性的结果很少。本文研究了整数线性算术在SMT下的一元可分解性。我们表明，这个决策问题是CONP-完全的，当monadically可分解，一个公式承认在最坏的情况下分解的指数大小。我们提供了一个新的应用程序，我们的结果字符串约束求解长度约束。然后，我们扩展我们的结果变元分解，谓词可以承认多个自由变量（相对于一元分解）。最后，我们给出了整数线性算术中的量词消去的一个应用，其中量词块中的变量，如果是独立的，可以用指数（而不是标准的双指数）爆破消除。
2020-04-26 cs.LO
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
在过去的十年中，我们已经目睹了一个令人印象深刻的进步，表现力和效率的可满足性模理论（SMT）解决技术。这给最先进的SMT求解器带来了以前难以解决的问题，特别是在软件和硬件验证领域。然而，许多感兴趣的SMT编码问题，也需要找到最佳wrt模型的能力。一些成本函数。在以前的工作中，即“优化模理论与线性有理成本函数- OMT（LAR UT）”，我们利用SMT解决处理成本函数的线性算术的最小化的理由，通过SMT和LP最小化技术的组合。在本文中，我们沿着三个方向推进了OMT方法：首先，我们通过SMT、LP和ILP最小化技术的组合，将其扩展到混合整数/有理数域上的线性运算;其次，我们开发了一个多目标版本的OMT，以便同时处理多个成本函数;第三，我们开发了一个OMT的增量版本，以便利用一些OMT可编码问题的增量性。OMT编码的验证问题上进行的实证评估表明，这些扩展的有用性和效率。
2015-01-16 cs.LO
A Modern View on MCSat
TU Wien（维也纳工业大学）
重新审视理论无关的MCSat框架作为证明系统，通过形式化其在Yices2求解器中的实现，纳入不同设计决策，给出通用理论无关规则方案并实例化，以展现基于MCSat的SMT推理现状。
2026-07-08 cs.LO
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
针对MCSat求解非线性整数算术SMT问题时赋值选择影响性能的问题，提出融合局部搜索的引导框架，结合加速爬山与可行集跳转实现于Yices2，并在SMT-LIB基准上完成评估。
2025-07-23 cs.LO
Advances in Symmetry Breaking for SAT Modulo Theories
对称破缺是一种常用的技术，它利用公式中变量和子句的对称性来减少SAT求解的搜索空间。其关键思想是首先确定属于同一对称类的赋值集，然后施加排序约束，称为对称性破坏谓词（SBP），使得这些赋值中只有一个（或一个小子集）被允许是原始SAT公式的解。虽然这项技术已被广泛利用在SAT文献，有很少的工作使用对称性破缺SAT模理论（SMT）。在SMT中，SAT理论中的逻辑约束与定义在非布尔变量（如整数、实数等）上的另一组理论运算相结合。SMT求解器通常使用SAT求解技术的组合，并通过调用理论求解器来增强。在这项工作中，我们采取了SAT对称性破缺的进展，并将其应用到域的SMT。我们的关键技术贡献是制定对称性破缺的布尔骨架变量，这是占位符的实际理论操作SMT解决。然后，这些SBP应用于SMT求解器的SAT求解部分。我们在最先进的SMT求解器CVC 4之上实现SBP理念。与最先进的方法相比，我们的方法可以在几个基准问题上获得更快的解决方案。我们的最终求解器是原始CVC 4求解器和基于SBP的求解器的混合体，与该类别中表现最好的CVC 4相比，在2018年和2019年SMT基准的QF_NIA类别中，分别可以解决高达3.8%和3.1%的问题。
2020-01-16 cs.LO
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic
本文提出了一个基于实例的一阶理论中量化公式可满足性决策过程的框架，包括其正确性，实现和评估。使用这个框架，我们推导出线性实数算术（LRA）和线性整数算术（LIA）公式与一个量词交替的决策程序。我们的程序可以集成到典型的SMT求解器使用的解决架构。从模型检验，静态分析和合成标准化基准的实验结果表明，我们的SMT求解器CVC 4中的程序的实现优于现有的工具，量化的线性运算。
2016-02-11 cs.LO
SMT(LIA) Sampling with High Diversity
College of Computer Science and Technology, Jilin University（吉林大学计算机科学与技术学院）；Key Laboratory of Symbolic Computation and Knowledge Engineering Ministry of Education, Jilin University（吉林大学符号计算与知识工程教育部重点实验室）；School of Software, Beihang University（北航软件学院）
针对软件和硬件测试需要多样化测试输入的问题，提出首个结合局部搜索与 CDCL(T) 技术的 SMT(LIA) 采样框架 HighDiv，通过引入边界感知移动算子和优化预处理机制，生成了比 MeGASampler 多样性更高的解。
2025-09-15 cs.AI cs.LO
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
抽象（以其各种形式）是模型检验中一种强大的既定技术;然而，当涉及无界数据结构时，它并不总是以令人满意的方式处理发散现象。加速是一种广泛应用的避免发散的方法，但它主要应用于整数规划。本文讨论了无界数组的加速转换关系问题，最终目标是避免抽象程序可达性分析过程中的发散。为此，我们首先设计了一种格式来计算在这个域中的加速度，然后我们展示了如何适应所谓的“单调抽象”技术，以有效地处理复杂的公式与嵌套的量词所产生的加速预处理。值得注意的是，我们的技术可以很容易地插入到抽象/细化循环，并大大有助于避免发散：与MCMT模型检查器进行的实验证明了我们的方法对具有无界数组的程序的有效性，如果单独应用加速和抽象/细化技术，则会失败。
2013-10-03 cs.LO
Invariant Checking for SMT-based Systems with Quantifiers
针对由 SMT 理论与量词定义的符号迁移系统，论文提出两种结合 IC3、隐式谓词抽象及下近似推广的全称归纳不变式检查算法，实验显示其统一处理能力和性能均具竞争力。
2024-02-29 cs.LO
Linear Integer Arithmetic Revisited
我们认为，线性整数规划的验证系统，如SMT求解器或定理证明器的背景下的可行性。虽然线性整数规划的可满足性是可判定的，但许多最先进的求解器为了提高效率而忽略了终止性。这是具有挑战性的设计一个解决方案，是终止和实际有效的。Jovanovic和de Zelia最近的工作是朝着这一方向迈出的重要一步。他们的算法CUTSAT是健全的，但一般不会终止。在本文中，我们扩展了他们的CUTSAT算法的细化推理规则，一种新型的冲突的核心，和一个专门的规则应用策略。这导致了我们的算法CUTSAT++，它保证了终止。
2020-10-23 cs.LO
Satisfiability Modulo Exponential Integer Arithmetic
本文提出将增量线性化方法扩展到带指数函数的整数算术SMT求解中，通过生成引理排除违反指数语义的模型，实验证明该方法在实践中非常有效。
2025-08-28 cs.LO
Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
本文针对智能合约验证中的非线性算术约束难题，研究并评估了Certora Prover使用的两种过近似技术，发现其能显著提升SMT求解器解决验证问题的数量。
2024-02-15 cs.LO
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
Stanford University（斯坦福大学）
本文提出了一种新的决策过程，用于支持常量数组的数组理论，能够处理任意索引域，并不局限于无限情况。
2026-07-22 cs.LO
Encoding Linear Constraints into SAT
Barcelogic（巴塞罗逻辑公司）；Technische Universität Berlin（柏林工业大学）；Monash University（莫纳什大学）
线性整数约束是组合问题中最重要的约束之一，因为它们在许多实际应用中是常见的。通常，与SAT模理论（SMT）、惰性子句生成（LCG）或混合整数规划（MIP）求解器相比，对合取范式的布尔可满足性（SAT）格式的编码在具有这些约束的问题中表现不佳。在本文中，我们探讨和分类SAT编码的线性整数约束。我们定义了新的SAT编码的基础上多值决策图，排序网络。我们比较不同的SAT编码的线性约束，并证明其中一个可能是更可取的。我们还比较SAT编码对其他解决方法，并表明他们可以比线性整数（MIP）求解器，有时比LCG或SMT求解器在适当的问题。将新的编码与惰性分解相结合，在运行时只对对发生的求解过程重要的约束进行编码，为许多涉及线性约束的高度组合问题提供了最佳选择。
2020-05-05 cs.AI cs.LO
Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
Institute of Computer Science, The Czech Academy of Sciences（捷克科学院计算机研究所）；Faculty of Information Technology, Czech Technical University in Prague（布拉格捷克理工大学信息技术学院）；Czech Institute of Informatics, Robotics and Cybernetics, Czech Technical University in Prague（布拉格捷克理工大学信息学、机器人学与控制论捷克研究所）
本文提出通过归纳论证认证全称量词和未解释函数符号可满足性的方法，应用于线性整数算术，证明了当前SMT求解器无法处理的公式可满足性。
2026-02-18 cs.LO
BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)
并发程序的程序验证是一个很大的挑战，由于一般的不可判定的结果。Petri网及其扩展在大多数工作中使用。然而，现有的基于Petri网的验证器很难是完整的和有效的。基本并行进程（BPP）作为Petri网的一个子类，可以作为描述和验证并发程序的模型，具有较低的复杂度。我们提出并实现了BPP的，第一个模型检查器，用于验证一个子类的CTL BPP。针对BPP的模型检验问题，提出了基于约束的算法，并用SMT求解器Z3处理公式。对于EF算子，我们将EF公式的模型检验归结为存在Presburger公式的可满足性问题。对于EG算子，我们给出了k步有界语义，并将EG公式的模型检验问题归结为线性整数运算的可满足性问题。此外，我们给演员通信系统（ACS）的过近似BPP的语义和评估BPP的演员通信系统从真正的Erlang程序生成。实验结果表明，BPPPERT在一系列Erlang程序的分支时间属性验证问题上比现有工具有更高的效率。
2021-10-25 cs.FL cs.LO
Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version)
我们提出了一种替代方法来解决硬件（HW）和软件（SW）分区问题，它使用基于可满足性模理论（SMT）的有界模型检验（BMC）结合使用开放多处理的多核支持。基于多核SMT的BMC方法允许基于模型检查器可用的处理器核数初始化许多验证实例。每个实例检查不同的最优值，直到满足优化问题。我们的目标是表明，多核模型检查技术可以是有效的，在特定情况下，找到最佳的解决方案的HW-SW分区问题使用基于SMT的BMC方法。实验结果表明，该方法与传统的线性规划算法和遗传算法相比具有更好的收敛性。
2015-09-08 cs.LO cs.SE
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
Ramsey Quantifiers in Linear Arithmetics
本研究提出一种可从LIA、LRA、LIRA三种线性算术SMT理论中消除拉姆齐量词的多项式时间算法，解决了相关良基性检查、一元可分解性等开放问题，并在原型测试中取得良好效果。
2023-11-07 cs.FL cs.LO
Local Search for Solving Satisfiability of Polynomial Formulas
非线性实数算术理论的模可满足性（Satisfiability Modulo the Theory of Nonlinear Real Arithmetic，简称SMT，NRA）涉及多项式公式的可满足性，多项式公式是具有整数系数和实变量的多项式方程和不等式的无量词布尔组合。在本文中，我们提出了一个局部搜索算法的一个特殊子类的SMT（NRA），其中所有的约束是严格的不等式。一个重要的事实是，给定一个含有$n$变量的多项式公式，公式中多项式的零水平集将$n$维实空间分解为100个分量（单元），并且每个多项式在每个单元中具有常数符号。我们的算法的关键点是一个新的操作的基础上真正的根隔离，称为细胞跳跃，更新当前分配沿给定的方向，使分配可以“跳”从一个单元到另一个。一个单元格跳跃可以调整多个变量的值，而传统的局部搜索操作，如SAT的翻转和SMT的临界移动（LIA），只改变一个变量的值。为了平衡成功率和效率，我们还设计了两级操作选择。此外，我们的算法可以很容易地推广到一个更广泛的子类SMT（NRA）的多项式方程线性关于一些变量是允许的。实验结果表明，该算法与现有的SMT求解器相比具有很好的竞争力，尤其是在高次多项式的公式上。
2023-03-21 cs.LO cs.SC
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
本文利用自动机与算术公式间的细粒度对偶，将位向量自动机与代数推理结合，提出以公式导数构造自动机状态并大规模优化的量化线性整数算术求解方法，原型性能媲美甚至超过前沿 SMT 求解器。
2024-05-18 cs.LO
Inferring Lower Runtime Bounds for Integer Programs
我们提出了一种技术来推断整数程序的最坏情况下的运行时复杂性的下限，在早期的工作相比，我们的方法不限于尾递归。我们的技术构造程序执行的符号表示使用迭代的框架，下近似程序简化。这种简化的核心是一种基于递归求解和排序函数变化的（欠近似）程序加速方法。之后，我们推导出的渐近下界从所得到的简化程序使用一个特殊用途的微积分和SMT编码。我们实现了我们的技术在我们的工具LoAT，并表明它推断出一个大类的例子的非平凡的下限。
2020-09-28 cs.LO cs.PL
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
计算克雷格插值的问题最近受到了很大的关注。在本文中，我们解决了一阶逻辑，这是服从有效的决策程序，称为满意度模理论求解器的一些重要片段的插值的有效生成的问题。我们做出以下贡献。首先，我们提供插值程序的几个基本理论的兴趣：理论的线性算术的有理数，差分逻辑的有理数和整数，UTVPI的有理数和整数。其次，我们定义了一种新的方法来插值的理论组合，适用于延迟理论组合方法。所提出的插值算法扩展了可满足性模理论的现有算法，从而保证了效率。我们的实验评估表明，MathSAT SMT求解器可以产生插值与较小的开销在搜索中，更有效地比其他竞争对手的求解器。
2009-06-24 cs.LO
ILP Modulo Theories
我们提出了整数线性规划（ILP）模理论（IMT）。IMT实例是一个非线性规划实例，其中一些符号在背景理论中有解释。在以前的工作中，IMT方法已被应用到工业合成和设计问题的实时限制所产生的波音787的发展。从运筹学到软件验证的许多其他问题通常涉及线性约束和优化。因此，一个通用的ILP模理论框架具有广泛应用的潜力。IMT发展的下一个合乎逻辑的步骤和本文的主要目标是提供理论基础。这是通过BC（T），分支和切割模T抽象转换系统来实现的。我们表明，BC（T）提供了一个健全的和完整的优化过程的ILP模T问题，只要T是一个可判定的，稳定的无限理论。我们将BC（T）的原型与领先的SMT求解器进行比较。
2013-04-08 cs.LO
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。
2023-05-24 cs.LO
Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (Short WST Version)
本研究提出一种模块化方法，将三角弱非线性循环的运行时间界研究成果用于整数程序复杂度分析，通过计算子程序局部界并提升为全局界，实现了现有顶尖工具无法完成的复杂度分析。
2023-07-19 cs.LO
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
本文提出一种模块化方法，将子程序转换为 twn-loops 计算局部运行时间界限并提升为全局界限，在工具 KoAT 中实现了对其他最先进工具无法处理的整数程序的复杂度分析。
2024-11-15 cs.LO
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
University of Bremen（不来梅大学）；DFKI GmbH（德国人工智能研究中心）
提出了一种验证前馈神经网络的方法，其中所有节点具有分段线性激活函数。这种网络通常用于深度学习，并且已被证明很难验证现代可满足性模理论（SMT）和整数线性规划（ILP）求解器。我们的方法的出发点是将整体网络行为的全局线性近似添加到验证问题中，这有助于对网络行为进行类似SMT的推理。我们提出了一个专门的验证算法，采用这种近似在搜索过程中，它推断出额外的节点相位的非线性节点在网络中的部分节点相位分配，类似于经典的SAT求解中的单位传播。我们还展示了如何从搜索过程中执行的分析步骤的结果中推断出额外的冲突条款和安全节点夹具。碰撞避免和手写数字识别的案例研究所产生的方法进行评估。
2017-08-02 cs.AI cs.LG cs.LO
Solving Modular Model Expansion Tasks
我们在这里描述的工作是一个研究计划的一部分，发展基础的声明解决搜索问题。我们认为模型扩展任务是代表搜索问题本质的任务，在搜索问题中，我们给出了一个问题的实例，并正在搜索满足某些属性的解决方案。这样的任务在人工智能、形式化验证、计算生物学中很常见。最近，模型扩展框架被扩展到处理多个模块。在本文中，受实际组合求解器的启发，我们介绍了一种算法来解决模块化系统的模型扩展任务。我们表明，我们的算法密切对应于在实践中所做的不同领域，如可满足性模理论（SMT），线性规划（ILP），回答集编程（ASP）。
2011-09-03 cs.LO
Quantifiers on Demand
自动程序验证是一个难题。即使对于线性代数上的转移系统，它也是不可判定的。用数组理论扩展转换系统，通过要求用普遍量化的公式进行推理和推理，使问题进一步复杂化。在本文中，我们提出了一个新的算法，Quic3，扩展IC3推断普遍量化的不变量的LIA和数组的组合理论。与其他使用IC3或SMT求解器作为黑盒的方法不同，Quic3仔细管理量化泛化（以构建量化不变量）和量词实例化（以检测量词存在时的收敛性）。虽然Quic3不能保证收敛，但它可以保证通过探索越来越长的执行来取得进展。我们在Z3的约束Horn子句求解器引擎中实现了Quic3，并通过应用Quic3来验证数组操作C程序的各种公共基准来进行实验。
2021-06-01 cs.LO cs.PL
CTL* model checking for data-aware dynamic systems with arithmetic
复杂动态系统的分析是形式化方法和人工智能的核心研究课题，系统与数据的组合建模在业务流程管理等应用中越来越重要。此外，流程挖掘技术现在被用来自动地从事件数据中挖掘流程模型，通常没有正确性保证。因此，需要验证技术的线性和分支时间属性，以确保所需的行为。在这里，我们考虑数据感知的动态系统与算术（DDSAs），这构成了一个简洁的，但表达形式主义的过渡系统与线性算术后卫。我们提出了一个CTL* 模型检验程序DDSAs依赖于一个有限状态的抽象，通过一组公式，捕捉变量配置。线性时间验证被证明是可判定的，在特定类别的DDSAs的约束语言或控制流被适当地限制。我们调查了几个这些限制的情况下，CTL*，积极和消极的结果：CTL* 验证被证明是可判定的单调性和整数周期性约束系统，但不可判定的反馈自由和有界回看系统。为了证明我们的方法的可行性，我们实现了它在基于SMT的原型ADA，显示出许多实际的业务流程模型可以有效地分析。
2022-05-18 cs.LO
CSS Minification via Constraint Solving (Technical Report)
压缩是一种被广泛接受的技术，旨在减少通过Web传输的代码的大小。我们研究的问题，缩小级联样式表（CSS）-事实上的语言样式的网页文件。传统上，CSS minifiers专注于简单的语法转换（例如缩短颜色名称）。本文提出了一种新的基于合并CSS文件中相似规则的压缩方法。我们考虑CSS文件的安全转换，它保留了CSS文件的语义。CSS文件的语义对文件中规则的顺序很敏感。为了自动识别最大限度地减少文件大小的规则合并机会，我们将规则合并问题简化为CSS图上的问题，即，节点加权的二分图，在边缘上具有依赖性排序，其中权重捕获字符的数量（例如，在选择器或属性声明中）。粗略地说，相应的CSS-图问题涉及最小化覆盖CSS-图并尊重边序的biclique（完全二部子图）序列的总重量。我们提供了第一个完整的形式化的CSS3选择器，并减少依赖检测，以满足量化器免费整数线性运算，高度优化的SMT求解器。为了解决上述NP难图优化问题，我们展示了如何有效地使用Max-SAT求解器。我们使用Max-SAT和SMT求解器作为后端实现了我们的算法，并对大约70个真实世界的例子进行了测试（包括前20个最受欢迎的网站）。在我们的基准测试中，我们的工具比六个著名的minifiers（不执行规则合并，但支持许多其他优化）节省了更多。我们的实验还表明，更好的节省可以实现与这六个minifiers之一相结合。
2018-12-07 cs.LO cs.PL
