Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
IC3 Modulo Theories via Implicit Predicate Abstraction
我们提出了一种新的方法来推广的IC3算法不变检查从有限状态到无限状态的过渡系统，表示在一些背景理论。该过程是基于IC3与隐式（谓词）抽象的紧密集成，隐式（谓词）抽象是一种表示抽象转换而不显式计算抽象系统的技术，并且相对于谓词的增加是增量的。在这种情况下，IC3只在抽象状态空间的布尔级别上操作，发现抽象谓词上的归纳子句。理论推理被限制在底层SMT求解器中，并在执行可满足性检查时透明地应用。当当前的抽象允许一个虚假的反例时，它通过发现和添加足够的新谓词集来改进。重要的是，这可以以完全增量的方式完成，而不会丢弃在前一次搜索中找到的子句。所提出的方法有两个关键优点。首先，与IC 3当前的SMT泛化不同，它允许处理广泛的背景理论，而不依赖于临时扩展，例如量词消去或特定于理论的从句泛化程序，这些程序可能并不总是可用的，而且可能效率低下。其次，与直接探索具体的转换系统相比，使用抽象可以显著提高性能，正如我们的实验所证明的那样。
2013-10-25 cs.LO cs.SE
Probabilistic Abstractions with Arbitrary Domains
Hermanns等人和Kattenbelt等人最近的工作已经将反例引导的抽象细化（CEGAR）扩展到概率程序。这些方法仅限于谓词抽象。我们提出了一种新的技术，基于Gulavani等人最近引入的抽象可达树，可以使用任意抽象域和加宽运算符（在抽象解释的意义上）。我们展示了如何合适的扩大运营商可以推导出循环不变量难以找到谓词抽象，并提出改进技术。
2011-06-16 cs.LO cs.PL
Enhancing Predicate Pairing with Abstraction for Relational Verification
关系验证是一种旨在证明两个不同程序片段或两个不同程序运行相关属性的技术。它已被证明，受约束的霍恩子句（CHC）可以有效地用于关系验证，通过应用CHC转换，称为谓词配对，它允许CHC求解器推断不同谓词的参数之间的关系。在本文中，我们研究了如何通过使用基于线性算术的各种抽象域（即，凸多面体的域和它的一些子域）。在提出了一个算法与抽象谓词配对，我们报告的实验，我们已经进行了一百多个关系验证问题，通过使用各种抽象域。实验已经进行了使用VeriMAP转换和验证系统，连同帕尔马多面体库（PPL）和Z3求解器的CHCs。
2017-09-14 cs.LO cs.SE
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
我们提出了一种方法来约束霍恩子句（CHC）验证相结合的三种技术：抽象的解释在一个域的凸多面体，专门化的约束条件在CHC使用抽象解释的查询答案转换的条款，和细化分裂谓词。的工作的目的是调查如何分析和转换工具开发的约束逻辑程序（CLP）可以适用于霍恩子句验证问题。凸多面体的抽象解释能够推导出复杂的不变量，当与传播约束的专业化结合使用时，它可以经常解决具有挑战性的验证问题。这本身就是一个贡献，但是当它失败时需要精化，并且如何精化凸多面体分析的问题还没有被研究很多。我们提出了一种改进技术的基础上插值来自一个反例跟踪，这些都是用来驱动基于属性的专业化，分裂谓词，进而导致更精确的凸多面体分析。专业化，分析和分裂的过程可以重复，以类似于CEGAR和迭代专业化方法的方式。
2014-12-03 cs.LO
Abstraction Logic: A New Foundation for (Computer) Mathematics
抽象逻辑是一种新的逻辑，是数学的基础。它结合了谓词逻辑和高阶逻辑的特征：抽象逻辑既可以被看作是高阶逻辑减去静态类型，也可以被看作是谓词逻辑加上运算符和变量绑定。我们认为，抽象逻辑是最好的基础逻辑可能，因为它最大限度地提高了简单性和实际的表达能力。这一论点得到了以下观察的支持：抽象逻辑比所有其他一般逻辑具有更简单的术语和更简单的证明概念。同时，抽象逻辑可以形式化直觉主义的和经典的抽象逻辑，并且对于这些逻辑和所有其他用等式扩展演绎逻辑的逻辑都是可靠和完备的。
2022-07-12 cs.LO
Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition
抽象谓词被认为是本文的抽象技术堆分离的配置，并作为真正的Prolog谓词直接翻译成相应的形式语言语法作为验证计划的中间堆状态。所提出的方法是基于规则的，因为抽象谓词是基于规则的，解析技术可以被解释为相应堆图的自动折叠/展开。
2019-06-01 cs.FL cs.LO cs.SC
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
A simple abstraction of arrays and maps by program translation
我们提出了一种处理数组的程序的静态分析方法，数组程序的语义和纯标量操作的语义之间有伽罗瓦连接。实现它的最简单的方法是通过自动地将数组程序语法转换为标量程序，然后使用任何静态分析技术（抽象解释、加速、谓词抽象等）分析标量程序。.).由此获得的标量不变量被翻译回原始程序作为普遍量化的数组不变量。我们说明了我们的方法上的各种例子，导致“荷兰旗”算法。
2015-06-12 cs.LO cs.PL
Simulation Algorithms for Symbolic Automata (Technical Report)
我们研究符号有限自动机（SFAs）上模拟关系的有效计算方法，即，有限自动机，其转换由字母符号上的谓词标记。在一种方法中，我们建立在Ilie，Navaro和Yu最初为经典有限自动机提出的算法的基础上，使用所谓的转换谓词的mintermisation对其进行修改。然而，这种解决方案生成谓词的所有布尔组合，这很容易导致转换数量的指数爆炸。因此，我们提出了两个更先进的解决方案。第一个仍然应用mintermisation，但以局部方式，减轻了指数爆破的大小。另一个集中在一个新的符号方式处理的过渡，我们需要牺牲原来的算法的计数技术（计数是用来减少从二次到线性的过渡的数量上的运行时间的依赖性）。我们进行了彻底的实验评估的所有算法，再加上几个进一步的替代品，表明他们都有自己的优点，在实践中，但明确表示，在大多数情况下，有效的治疗符号转换是更有益的计数。
2018-07-27 cs.FL cs.LO
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
分离逻辑的符号堆片段已被积极开发和提倡用于验证计算机程序的存储器安全性质。目前，其最大的挑战之一是有效地证明包含归纳堆谓词的蕴涵。这些蕴涵通常是在验证操作复杂数据结构（如链表、树或图）的程序时生成的证明义务。为了帮助证明这样的蕴涵，本文介绍了一个引理合成框架，自动发现引理，作为尤里卡步骤的证明。数学归纳法和基于模板的约束求解是我们框架的两大支柱。为了导出给定蕴涵的支持引理，框架首先从蕴涵的堆结构中识别可能的引理模板。然后，它建立每个模板的变量之间的未知关系，并进行结构归纳证明，以产生这些关系的约束。最后求解约束条件，找出未知关系的实际定义，从而发现引理。我们已经将这个框架集成到一个原型证明器中，并在各种蕴涵基准上进行了实验。实验结果表明，我们的引理合成辅助证明器可以证明许多蕴涵，不能处理现有的技术。这个新提议为自动推理复杂的归纳堆谓词提供了更多的机会。
2017-11-08 cs.LO cs.PL
Interpretable and Explainable Logical Policies via Neurally Guided Symbolic Abstraction
Technical University of Darmstadt（达姆施塔特工业大学）；National Research Center for Applied Cybersecurity（国家应用网络安全研究中心）；Eindhoven University of Technology（埃因霍温理工大学）；Hessian Center for AI (hessian.AI)（黑森人工智能中心）；German Research Center for AI (DFKI)（德国人工智能研究中心）
本文提出NUDGE框架，通过神经引导的可微逻辑规则搜索，构建兼具可解释性与可说明性的策略，其性能优于纯神经网络且适应不同环境规模。
2023-10-25 cs.AI cs.CL cs.LG
ANDRE: An Attention-based Neuro-symbolic Differentiable Rule Extractor for Inductive Logic Programming
Dept. of Mechanical and Aerospace Engineering, George Washington University, USA（机械与航空航天工程系，乔治华盛顿大学）；Dept. of Mechanical Engineering Sciences, University of Surrey, UK（机械工程科学系，萨里大学）
提出ANDRE框架，通过注意力驱动的可微逻辑算子优化连续规则空间，实现从概率数据中学习一阶逻辑规则，在噪声环境下保持鲁棒性和可解释性。
2026-05-31 cs.AI cs.LG cs.LO
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
本文在 ADG 框架中提出 TATL 的即时符号验证算法，并通过推广包含检查与新型抽象显著加速，性能优于朴素方法及 Uppaal Tiga。
2025-06-09 cs.LO
Enhancing Symbolic Machine Learning by Subsymbolic Representations
Johannes Gutenberg Universität Mainz（莱茵河畔明斯特大学）
针对现有神经符号系统在简单判别式机器学习等场景效率偏低，研究提出为符号机器学习方案引入神经嵌入以增强性能，经三个真实域实验显示该方法F1分数优于所有基线，且可拓展至多类应用场景。
2025-06-17 cs.AI cs.LO
Differentiable Inductive Logic Programming in High-Dimensional Space
Czech Academy of Sciences Institute of Computer Science（捷克科学院计算机科学研究所）；University of Innsbruck（因斯布鲁克大学）；University of Melbourne（墨尔本大学）
本文扩展 δILP，利用高维梯度下降实现大规模谓词发明，使可微归纳逻辑程序设计能在不预设解结构的情况下解决现有神经符号 ILP 系统无法完成的任务。
2025-01-08 cs.AI cs.LO
On the Verification of a WiMax Design Using Symbolic Simulation
在自顶向下的多层次设计方法中，在更高抽象层次上的设计描述被逐步细化到最终实现。基于仿真的技术传统上被用于验证这种模型改进不会改变设计功能。不幸的是，利用计算机模拟，不可能在合理的时间内完全检查设计变换是否正确，因为这样做所需的测试模式的数量随着系统状态变量的数量呈指数级增加。在本文中，我们提出了一种方法，用于验证在设计过程中产生的模型在更高的抽象层次的设计规范的一致性。我们使用递归方程的序列建模系统的行为。然后，我们使用符号模拟与等价性检查和属性检查技术的设计验证。使用我们提出的方法，我们已经验证了三个WiMax系统模型在不同层次的设计抽象的等效性，以及这些模型上的各种系统属性的正确性。我们的符号建模和验证实验表明，所提出的验证方法提供了其数值对应的性能优势。
2013-07-31 cs.LO
symQV: Automated Symbolic Verification of Quantum Programs
我们提出了symQV，一个符号执行框架，用于在量子线路模型中编写和验证量子计算。symQV可以自动验证量子程序是否符合一阶规范。我们正式介绍了一个符号量子程序模型。这允许在SMT公式中编码验证问题，然后可以使用delta-完全决策过程进行检查。我们还提出了一个抽象技术，以加快验证过程。实验结果表明，该抽象将symQV的可扩展性提高了一个数量级，可以扩展到具有24个量子比特（2^24维状态空间）的量子程序。
2022-12-05 cs.LO quant-ph
Inference of Abstraction for a Unified Account of Reasoning and Learning
Cardiff University（卡迪夫大学）
受神经科学贝叶斯方法启发，提出统一解释推理与学习的概率推断理论，将推理视为通过抽象从数据推导符号知识的过程，并通过逻辑证明和MNIST数据集验证其正确性。
2024-02-14 cs.AI cs.LG cs.LO
The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
在分离逻辑中用于检验指针程序的表段谓词非常适合于表示单链表的属性。我们研究了在完全无量词的分离逻辑中加入ls的效果，分离合取和蕴涵，这是由最近设计的新片段所激发的，在新片段中，所有这些成分都被无差别地使用，并且验证工具开始处理魔杖连接词。这是一个非常自然的扩展，迄今为止还没有被研究过。我们表明，没有分离的含义的限制，可以解决在多项式空间中使用适当的抽象记忆状态，而完整的扩展是不可判定的减少从一阶分离逻辑。当ls被添加时，从计算的角度也研究了逻辑和片段的许多变体，提供了关于将可达性谓词添加到无量词分离逻辑的许多结果。
2021-02-28 cs.LO
Feedback Refinement Relations for the Synthesis of Symbolic Controllers
University of the Federal Armed Forces Munich（联邦国防军大学）；Technical University of Munich（慕尼黑工业大学）
本文提出了一种抽象和细化方法，用于自动控制器合成以满足通用预定义规范。控制器仅需量化状态信息，通过静态量化器与系统接口，并通过反馈细化关系确保鲁棒性和可证明性。
2017-01-02 cs.LO cs.SY eess.SY
Symbolic Control for Stochastic Systems via Finite Parity Games
考虑离散时间演化的随机非线性系统满足ω-正则规范的最大概率计算问题。这个问题减少后，自动机理论的建设，找到最大的概率满足奇偶校验条件（可能是混合）状态空间。虽然表征精确的满意概率是开放的，我们表明，这个概率的下限可以通过以下方式获得：（I）计算定性获胜区域的欠近似，即，国家的奇偶校验条件可以强制执行几乎肯定，以及（II）计算达到这个定性的获胜区域的最大概率。我们方法的核心是一种技术，通过将原始系统作为2.5人奇偶博弈的有限状态抽象，象征性地计算步骤（I）中定性获胜区域的欠近似。我们的抽象过程只使用概率演化的支持，它不使用精确的数值转移概率。我们证明了抽象的2.5人博弈中的获胜集导致了原始综合问题中的定性获胜区域的欠近似，以及解决它的策略。通过将这些贡献与（a）求解2.5人博弈的符号不动点算法和（b）随机非线性系统中现有的可达性策略综合技术相结合，我们得到了一个基于抽象的算法，用于找到最大满意概率的下界。我们已经在Mascot-SDS中实现了基于抽象的算法（Majumdar等人，2020年），在那里我们将概述的抽象步骤与我们最近的工具FairSyn相结合。我们评估了我们的实现上的非线性模型的扰动开关从文献。我们的表现优于最近提出的解决这个问题的大幅度的工具。
2022-09-29 cs.LO cs.SY eess.SY
Ordered Counter-Abstraction
我们引入了一个新的符号表示的基础上原来的概括反抽象。与经典的反抽象（用于分析具有无序或非结构化拓扑的参数化系统）不同，新的表示是为证明线性有序参数化系统的性质而定制的，即，系统与任意多个有限进程放置在一个数组中。数组中的相对位置捕获进程的相对优先级。这些系统的子系统是任意长度的有限字。进程使用受其相对优先级约束的全局转换进行通信。直观地说，符号表示的元素有一个基和一组计数器。它表示遵守计数器所施加的约束的配置，并将base作为子字。我们使用新的表示在一个统一的和自动的反例指导的细化计划。我们引入了一个松弛算子，允许一个良好的准序参数的细化循环的每次迭代的终止。我们解释了如何改进松弛以系统地剔除误报。我们实现了一个工具来说明一些参数化系统的方法。
2012-03-31 cs.LO
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
带有归纳谓词的分离逻辑公式之间的蕴涵，也称为符号堆，已经被证明对于一大类归纳定义是可判定的。最近，提出了一个2-EXPTIME算法，并建立了一个EXPTIME硬界限，但没有精确的下限是已知的。在本文中，我们证明了决定谓词原子之间的蕴涵是2-EXPTIME困难的。证明是基于减少从指数空间有界交替图灵机的成员问题。
2020-04-16 cs.LO
A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
我们开发了一个双指数决策过程的可满足性问题的保护分离逻辑-一个新的片段的分离逻辑具有用户提供的归纳谓词，布尔连接词，分离连接词，包括限制（保护）版本的否定，魔术棒，和septraction。此外，我们表明，上述任何连接词的警卫下降导致一个不可判定的片段。我们进一步应用我们的决策过程的原因蕴涵在流行的符号堆片段的分离逻辑。特别是，我们获得了一个双指数决策过程之间的蕴涵（无量词）符号堆与有界树宽（SLIDbtw）的归纳谓词定义-分离逻辑的最具表现力的可判定片段之一。再加上最近显示的2 ExpTime-hardness在所述片段中的蕴涵，我们得出结论，SLIDbtw的蕴涵问题是2 ExpTime-complete-从而关闭了以前开放的复杂性差距。
2021-04-20 cs.LO
