Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)
我们提出了一个懒惰的决策过程的逻辑WSkS。它建立了一个基于术语的符号表示的状态空间的树自动机（TA）构造的经典WSkS决策过程。经典的决策过程通过自底向上的遍历将符号表示转换为TA，然后测试其语言非空性，这对应于公式的可满足性。另一方面，我们从顶部开始评估表示，动态构建状态空间，并利用机会修剪掉与语言空虚测试无关的状态空间部分。为了做到这一点，我们需要将我们前面的逻辑线性片段（所谓的WS1S）过程中使用的语言项（表示语言派生）的概念扩展为自动机项。我们实现了我们的决策过程，并确定了我们的原型实现明显快于Mona工具中实现的经典过程的公式类。
2019-05-21 cs.FL cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Bounded Structural Model Finding with Symbolic Data Constraints
University of Leicester（莱斯特大学）
本文提出Maude Model Finder，通过符号可达性实现结构求解，无需定制生成器，提供有限约束驱动的演算，支持对称性减少，并在声明范围内证明终止性、正确性和完备性。
2026-03-23 cs.LO
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
本文提出基于层级同步树自动机的量子电路符号验证方法，将门操作复杂度降至至多二次方，并支持参数化验证，实验表明其可处理规模远超现有工具的问题。
2024-10-24 cs.FL cs.LO
String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)
字符串分析是推理程序如何操作字符串的问题。它有许多应用程序，包括自动检测跨站点脚本（XSS）。流行的字符串分析技术包括符号执行，其核心使用字符串（约束）求解器。这样的求解器通常会推理以字符串理论表达的约束，并将连接运算符作为原子约束。近年来，研究人员开始认识到在串接弦理论中引入替换所有算子和有限转换的重要性。这样的字符串操作通常对于Web应用程序中的XSS漏洞推理至关重要，特别是对消毒功能和隐式浏览器转换（例如innerHTML）进行建模。在本文中，我们提供了第一个字符串求解器，可以原因涉及连接和有限转换的约束。此外，它对几个重要的片段（例如直线片段）具有完整性和终止性保证。在本文中解决的主要挑战是禁止最坏情况下的理论的复杂性。为此，我们提出了一种方法，利用简洁的交替有限自动机作为字符串约束的简洁符号表示。交替不仅在表示换能器的布尔组合时提供了空间上的指数节省，而且还提供了简洁表示换能器和级联的否则昂贵的组合的可能性。关于AFA语言的空性的推理需要在指数大小的图中进行状态空间探索，为此我们使用模型检验算法（例如IC3）。我们已经实现了我们的算法，并证明了它的效力，来自XSS和文献中的其他例子的基准。
2020-10-29 cs.LO
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic
信号时序逻辑监测的数值模拟轨迹已经成为一种有效的方法来近似验证的连续和混合系统。在本报告中，我们探索了STL属性的精确验证程序，该程序基于对Flow* 验证积分器生成的泰勒模型流管形式的验证痕迹进行监控。我们将探讨与Flow* 符号流管表示的紧密集成如何实现更精确、更高效的监控。然后，我们展示了如何通过引入掩码，将流管监测限制在与复杂命题的整体真相相关的时间区域的方法的属性导向的改进来大幅提高监测的性能。最后，我们将这些方法的实现应用于验证一个具有挑战性的连续系统的属性，评估我们的程序的每个方面对监控性能的影响。
2020-08-14 cs.LO
Proceedings 36th International Conference on Logic Programming (Technical Communications)
自1982年在马赛举行第一次会议以来，ICLP一直是展示逻辑编程研究的首要国际活动。在逻辑编程和相关领域的所有领域征求贡献，包括但不限于：-基础：语义学，形式主义，集合编程，非单调推理，知识表示。- 声明式编程：推理引擎，分析，类型和模式推理，部分求值，抽象解释，转换，验证，验证，建模，分析，测试，基于逻辑的领域特定语言，约束处理规则。- 相关范例和协同作用：归纳和协同归纳逻辑程序设计、约束逻辑程序设计、与SAT、SMT和CSP求解器的交互、用于类型推断和定理证明的逻辑编程技术、论证、概率逻辑程序设计、与面向对象和函数式编程的关系、描述逻辑、神经符号机器学习、混合深度学习和符号推理。- 实施情况：并发和分布，对象，协调，移动性，虚拟机，编译，高阶，类型系统，模块，约束处理规则，元编程，外部接口，用户界面。- 应用领域：数据库、大数据、数据集成和联合、软件工程、自然语言处理、Web和语义网、代理、人工智能、生物信息学、教育、计算生命科学、教育、网络安全和机器人技术。
2020-09-19 cs.AI cs.LO cs.PL
Negated String Containment is Decidable (Technical Report)
本文解决了不包含字符串谓词可判定性的长期开放问题，证明了在正则语言约束下该谓词及其与无链字方程结合的可判定性。
2025-06-30 cs.FL cs.LO
CertiStr: A Certified String Solver (technical report)
在过去的十年中，字符串理论是SMT社区中研究最多的逻辑理论之一，这是由于字符串操作容易出错的性质，这通常会导致安全漏洞（例如跨站点脚本和代码注入）。这些理论的大多数现有决策过程和求解器本身是复杂的;它们在算法上是复杂的，并且还必须处理非常丰富的运算词汇。这导致了大量的bug，例如通过模糊检测发现的。在本文中，我们提出了CertiStr，一个认证的实现字符串约束求解器的理论与串联和常规的约束。CertiStr旨在使用基于正则约束的符号表示的前向传播算法来解决字符串约束，该算法作为符号自动机，返回三个结果：sat，unsat和unknown，并且保证对于串联依赖关系为非循环的字符串约束终止。该实现已在Isabelle/HOL中开发并证明是正确的，通过该实现生成了OCaml中的有效求解器。我们证明了CertiStr的有效性和效率对标准的卡鲁扎基准，其中80.4%的测试是在字符串约束片段的CertiStr。在这80.4%的测试中，CertiStr可以在60秒内解决83.5%（即CertiStr返回sat或unsat）。
2021-12-11 cs.FL cs.LO cs.PL
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。
2017-10-30 cs.DC cs.FL cs.LO
Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）
本文提出基于尼尔森变换的图神经网络引导词方程求解算法，通过五种图表示编码结构信息，将拆分决策作为多分类任务，实现求解器DragonLi，在可满足问题及多方程合取上表现优异。
2024-11-19 cs.AI cs.CL cs.LG
Technical-Report: Automating Recoverability Proofs for Cyber-Physical Systems with Runtime Assurance Architectures
本文形式化RTA保护下CPS的决策采样时间充分性与时间有界可恢复性问题，并通过集成Maude与Z3的模SMT符号重写自动生成恢复证明。
2023-04-23 cs.LO cs.SE
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
本文提出 CryptoVampire，首次通过一阶形式化、子项关系处理及 Vampire 饱和推理，全自动完成 BC Logic 中密码协议轨迹属性证明。
2024-04-05 cs.CR cs.LO
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report)
我们考虑的问题，验证系统的活性有限，但无界，过程的数量，通常被称为参数化系统。这类系统的典型例子包括分布式协议（例如哲学家就餐问题）。与验证安全性的情况不同，证明活性仍然被认为是极具挑战性的，特别是在系统中存在随机性的情况下。在本文中，我们考虑任意（包括不公平的）干扰下的活性，这通常被认为是一个理想的属性在文学的自稳定系统。我们介绍了一种自动的方法证明活性的随机参数化系统在任意的干扰。将活性视为两个玩家之间的可达性游戏（在过程和过程之间），我们的方法是CEGAR方法，该方法合成了过程的进度关系，该过程可以象征性地表示为有限状态自动机。该方法是增量的，并利用了Angluin风格的L* 学习和SAT求解器。我们的实验表明，我们的算法能够自动证明著名的随机分布式协议，包括莱曼拉宾随机用餐哲学家协议和随机自稳定协议（如以色列Jalfon协议）的活性。据我们所知，这是第一个可以证明随机协议活性的全自动方法。
2016-06-05 cs.LO cs.PL
Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report
时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。
2020-09-16 cs.FL cs.LO
$Π$-NeSy: A Possibilistic Neuro-Symbolic Approach
Paris-Panthéon-Assas University（巴黎先贤祠-阿萨斯大学）；Univ. Artois（阿图瓦大学）；CNRS（法国国家科学研究中心）；CRIL（CRIL研究所）；Institut Universitaire de France（法国大学研究院）
本文提出Π-NeSy方法，将神经网络输出转换为可能性分布并与基于可能性规则的系统结合，通过矩阵和方程组设计实现高效推理和规则参数学习，在MNIST加法和数独任务上优于现有神经符号方法。
2025-04-09 cs.AI cs.LG cs.LO
Logic of Hypotheses: from Zero to Full Knowledge in Neurosymbolic Integration
University of Padua（帕多瓦大学）；Fondazione Bruno Kessler（布鲁诺·科斯勒基金会）；University of Bozen-Bolzano（博赞-博尔扎诺大学）
本文提出LoH语言，结合数据驱动规则学习与符号先验和专家知识，实现神经符号整合的灵活统一，并通过模糊逻辑实现可微计算图编译。
2026-05-15 cs.AI cs.LG cs.LO
