A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory
这项工作提出了一个Prolog方言的表达性和自动化的发现和优先级的问题。给定某个类C程序，如果动态内存在运行时被分配、更改和释放，那么对所需动态内存的描述就是堆规范。根据给定规范检查计算的存储器状态是动态存储器验证。本文只考虑了Hoare演算中的形式规范和验证。发现的问题包括：无效分配、存储单元中的（临时）不可用数据、过多的存储器分配、意外区域中的（意外）堆更改等。过多的内存分配现在已经被像Valgrind这样的内存分析器成功地解决了。从本质上讲，这些领域的论文并没有带来任何大的突破。可能的原因还包括由于更多的可用内存和并行线程而导致的张力降低。然而，从Apt开始，与可变模式有关的问题尚未得到解决-既没有完全解决，也没有以可接受的方式解决。过去几十年的研究成果一次又一次地表明，堆问题仍然存在，仍然很复杂，仍然很重要。Peter O 'Hearn在2016年做出了重大贡献，他因其空间堆操作的并行方法而获得哥德尔奖。
2021-04-04 cs.FL cs.LO cs.PL
A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and Disjunction
在本文中，我们回顾了现有的点到分离逻辑的动态内存推理，我们发现，不同的使用堆分离往往是一个障碍。因此，两个总的和严格的空间堆操作堆图上提出，合取和析取-类似于逻辑合取。堆合取意味着存在一个可连接的空闲堆顶点，或者提供了一个显式的目标顶点。基本上，Burstall的性质不会改变。堆是指一个任意的简单有向图，它是有限的，可以包含代表类对象的复合顶点。限制任意堆内存访问，以及类型双关、后期类绑定和其他限制。新的逻辑的性质进行了调查，并作为一个结果组的属性。期望堆和表面堆都是可指定的。等价变换可能会使表示的堆不一致，尽管这些可以通过给出的两个通用线性规范化步骤检测和修补。这些属性有助于激励以后全面介绍堆上的一组等价物，以便将来工作。部分堆被认为是一种有用的规范技术，有助于减少规范的不完整性问题。最后，所提出的逻辑可以被考虑用于对象约束语言的扩展。
2019-05-30 cs.FL cs.LO
A separation logic for sequences in pointer programs and its decidability
Peking University（北京大学）；Guangzhou University（广州大学）；Zhengzhou University（郑州大学）
分离逻辑及其变体可以描述指针程序的各种属性。然而，当涉及到序列的属性时，人们可能会发现很难形式化。为了处理变长序列和多级数据结构的属性，我们提出了序列堆分离逻辑，它将序列集成到堆操作程序的逻辑推理中。序列变量上的量词和存储序列的单例堆（序列单例堆）是我们逻辑中的新成员。进一步，我们研究了两个片段的可满足性问题。序列-堆分离逻辑的命题片断是可判定的，程序变量有2个交替、序列变量有1个交替的片断是不可判定的。此外，我们探索与前趋范式的逻辑的可判定和不可判定的片段之间的边界。
2023-01-16 cs.CL cs.LO
A proof-theoretic approach to abstract interpretation
Google Inc.（谷歌公司）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Johannesburg（约翰内斯堡大学）；University of Luxembourg（卢森堡大学）；INRIA（法国国家信息与自动化研究所）
本文通过将逻辑系统与有限抽象系统关联，提出了一种生成与抽象格同构的Lindenbaum-Tarski代数的逻辑的通用程序，并建立了相应的可靠性和完备性结果。
2026-05-26 cs.LO math.LO
Fully Automated Shape Analysis Based on Forest Automata
森林自动机（FA）最近被提出作为复杂堆结构的形状分析工具。FA以树自动机元组的形式对堆图的树分解集合进行编码。为了表示复杂的堆图，FA的概念允许提供用户定义的FA（称为框），这些框编码形状图的重复图形模式，以用作其他更高级别FA的字母符号。在本文中，我们提出了一种新的技术，自动学习FA被用作框，避免了手动提供它们的需要。此外，我们提出了一个显着的改进，在分析中使用的自动机抽象。其结果是一种高效的全自动分析，甚至可以处理像跳表这样复杂的数据结构，其性能可与基于分离逻辑的最先进的全自动工具相媲美，然而，它只专门处理链表。
2013-04-21 cs.FL cs.LO
Abstracting Probabilistic Models: A Logical Perspective
University of Edinburgh（爱丁堡大学）；Alan Turing Institute（艾伦·图灵研究所）
抽象是一种广泛应用于科学的强大思想，通过省略不相关的细节，在更易处理的搜索空间中对系统的行为进行建模、推理和解释。虽然抽象的概念已经成熟的确定性系统，抽象的概率模型的情况下尚未完全理解。在本文中，我们提供了一个语义框架，分析这种抽象的第一原则。我们开发的框架一般的方式，允许表达语言，包括基于逻辑的承认关系和层次结构与随机原语。我们激励一个高层次的模型和它的低层次的对应之间的一致性的定义，但也治疗的情况下，当高层次的模型是缺少关键信息存在于低层次的模型。我们证明属性的抽象，无论是在参数的水平，以及模型的结构。我们的结论与一些意见，如何抽象可以自动派生。
2020-01-13 cs.AI cs.LG cs.LO
Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional
我们定义了一个递归类型的λ演算的语法和约简关系，并给出了一个并行的条件函数。减少显示为融合性。我们将递归类型解释为受限形式的信息系统，我们称之为素系统。一个指称语义定义与此解释。定义了项的语法范式逼近，证明了逼近定理：项的语义等于其逼近的语义的极限。证明使用包含谓词（逻辑关系）。对于布尔值的观察，语义是足够的。在平行格功能的存在下，它也是完全抽象的。
2008-06-11 cs.LO
Collapsing Threads Safely with Soft Invariants
规范抽象是一种静态分析技术，它将状态表示为3值逻辑结构，并产生有限的抽象系统。尽管提供了一个有限的边界，这些抽象可能仍然遭受状态爆炸问题。值得注意的是，对于具有任意交错的并发程序，如果状态中的线程基于其位置被抽象，则位置的数量将是状态空间大小的组合因子。我们提出了一种方法，使用规范的抽象，避免这种状态爆炸的“崩溃”的所有线程在一个状态到一个单一的抽象代表。通过定义条件“软不变”插装谓词，保留了将被抽象丢失但验证所需的线程属性。这种技术是用来适应以前的模型验证非阻塞并发数据结构算法的线性化，从而导致指数较小的状态空间。
2015-12-31 cs.LO
Logical Characterization of Coherent Uninterpreted Programs
一个未解释的程序（UP）是一个程序，其语义定义在理论上的未解释的功能。这是等价性检查、编译器优化和程序验证中常用的抽象。虽然简单，但该模型足够强大，可以对计数器自动机进行编码，因此不可判定。最近，一类UP程序，称为相干，已被提出并证明是可判定的。我们提供了一个替代的，合乎逻辑的表征，这一结果。具体来说，我们证明了每一个相干程序是一个有限状态系统的双相似。此外，一个连贯程序的归纳不变量可以用一个公式表示，该公式的项的深度至多为1。我们还表明，原来的证明，通过自动机，只适用于一元未解释的功能的程序。虽然这项工作是纯理论的，它提出了一种新颖的抽象，是完整的连贯的程序，但可以合理地用于任意的未解释（和部分解释）的程序。
2021-07-26 cs.FL cs.LO
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
程序模块理论对语言设计者来说很有意义，不仅因为它对编程的实际重要性，还因为它是语言设计中三个基本问题的联系：阶段区分，计算效果和类型抽象。我们贡献了一个新的“合成”采取程序模块，将模块作为基本的结构，在通常的嫌疑人之前的模块演算（种，构造函数，动态程序）呈现为派生概念的模态类型理论帐户的阶段区别。我们简化了类型抽象的帐户（体现在模块函子的生成性）通过一个松散的模态，封装计算效果。我们的主要结果是程序模块演算的雷诺兹抽象定理的（重要的）证明相关和相敏的推广，基于一种称为参数结构的新型逻辑关系。参数化结构将经典参数化的证明无关关系推广到证明相关的家族，其中可能有非平凡的证据证明两个程序的相关性-简化了类型集合上的强和的元理论，因为虽然不可能有“关系分类关系”，但很容易容纳“家族分类小家族”。使用的洞察力，逻辑关系/parametricity本身是一种形式的语法和语义之间的相位区分，我们贡献了一个新的综合方法相分离parametricity的口号“逻辑关系作为类型”的基础上，迭代我们的模态帐户的相位区分。然后，要在一个抽象类型的两个实现之间构造一个模拟，只需编写第三个实现，其类型组件携带表示不变量。
2021-05-14 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
Compositional Verification in Concurrent Separation Logic with Permissions Regions
本文提出带权限区域的 CSL-Perm 组合式验证系统，通过可推断框架规则残余堆的蕴涵过程实现线程与函数调用推理，并经 CoSl 工具验证其优势。
2025-10-06 cs.LO cs.PL
Extending Logical Neural Networks using First-Order Theories
Yale University（耶鲁大学）
逻辑神经网络（LNN）是一种结合了神经网络的学习能力和形式逻辑系统的符号推理能力的体系结构。LLN为程序员提供了通过逻辑公式隐式修改神经网络底层结构的能力。在本文中，我们利用这种抽象来扩展LNN，通过一阶理论来支持等式和函数符号。这种扩展通过显著增加LNN可以处理的问题类型来提高LNN的能力。作为概念的证明，我们增加了对一阶理论的平等IBM的LNN库的支持，并演示了如何引入这允许LNN库现在的原因表达式，而不需要作出唯一的名称假设。
2022-08-11 cs.AI cs.LO
A New Perspective for Hoare's Logic and Peano's Arithmetic
Hoare逻辑是证明程序正确性的公理系统，它已被扩展为一种分离逻辑，用于对可变堆结构进行推理。我们在Peano算术$PA$中发展了Hoare逻辑最基本的最强后置条件逻辑结构。设$p\in L$和$S$为任意while程序。$\textbf{N}$ -可计算函数$f_S^{\textbf{N}}$的算术可定义性导致$S$与$SP(p,S)$分离，它定义了$p$和$S$在$\textbf{N}$上的最强后置条件，从而在$PA$中得到等价但更有意义的形式.从Hoare逻辑到PA的约化，再加上定义良好的底层语义，可以得出Hoare逻辑相对于$PA$理论是健全和完备的，这与Cook意义上的相对完备性不同。最后，我们讨论了两种方法来扩展可计算性从标准结构的非标准模型的$PA$。
2013-11-19 cs.LO
Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)
我们研究具体层模型的调用值高阶语言递归。我们的家庭层模型是一个推广的许多例子，从文献中，如模型的概率和可微规划，完全抽象的逻辑关系模型。我们以综合域理论的精神来对待递归。我们提供了一个一般的建设提升单子从一类允许的单态在现场的层范畴。这样，我们得到了一个家庭的模型参数化的具体网站和一类单态，我们证明了一个一般的计算充分性定理。
2022-05-31 cs.LO cs.PL math.CT
On Algebraic Abstractions for Concurrent Separation Logics
并发分离逻辑的特点是在并行组合和成帧时状态所有权的转移。支撑所有权转移的代数结构是部分交换幺半群（PCM）。现有的研究主要从逻辑的角度考虑所有权转移，而相对较少注意代数的考虑。本文利用保结构的部分函数（即，态射）之间的PCM，以及分离关系的相关概念。结构的态射是代数和范畴论中的标准概念，但在分离逻辑中还没有普遍使用过。分离关系是二元关系，它推广了不相交性，并描述了态射保持结构的输入。这两个抽象通过实现编写规范的简洁方式，通过提供在所有权转移下保留的线程状态的抽象视图，以及通过实现从现有PCM中构造新PCM的用户级构造，来促进验证。
2021-03-04 cs.LO cs.PL
Compiling Arguments in an Argumentation Framework into Three-valued Logical Expressions
Kwansei Gakuin University（关西学院大学）
本文提出了一种直接从完备性条件计算一般分配子的新方法。一般分配器是论证框架的所有完整标记的抽象。任何完整的标记都是通过将逻辑常量赋给变量从通用分配器中获得的。我们在以前的工作中证明了一般分配子的存在性。然而，构造需要我们枚举框架的所有完整标签，这使得计算非常慢。本文提出的方法使我们能够计算一般的分配器，而无需枚举完整的标签。它还提供了本地分配的解决方案，产生语义的框架的子集。我们展示了两个应用程序的一般分配器，稳定性，和一个新的概念框架，称为arity。此外，该方法，包括局部分配，适用于广泛的扩展框架，如集攻击的论证框架，双极论证框架，抽象的辩证框架。
2019-11-04 cs.AI cs.LO
Abstract Effects and Proof-Relevant Logical Relations
我们引入一种新的变体的逻辑关系，映射类型不仅是部分等价关系的价值观，因为通常这样做，而是证明相关的概括，即setoids。setoid的对象建立了值存在于语义类型中，而它的态射被理解为语义等价的证明。向证明相关性的过渡解决了传统克里普克逻辑关系中对未来世界使用存在量化所引起的两个众所周知的问题：可容许性失败和虚假的函数依赖。我们说明了新的格式与两个应用程序：一个直接风格的验证皮茨和斯塔克的等价“新”和指称语义的区域为基础的效果系统，支持类型抽象的意义上，只有外部可见的效果需要跟踪;不可观察的内部修改，如重组的搜索树或懒惰的初始化，可以算作“纯”或“只读”。这种“虚构的纯粹性”使模块的客户能够比传统效果系统更好地验证基于效果的程序等效性。
2012-12-22 cs.LO cs.PL
An Improved Proof-Theoretic Compilation of Logic Programs
在以前的工作中，我们表明，逻辑编程编译可以给出一个通用的抽象逻辑程序设计语言的证明理论的理由，并证明了这种技术的情况下，遗传Harrop公式及其线性变体。编译后的子句本身就是逻辑公式，除了在与它们的头相匹配的原子目标上存在二阶抽象。在本文中，我们重新审视我们以前的结果，以更详细和更充分的逻辑理由，消除这种虚假的抽象。然后，我们改进所得到的技术，以有效地支持模式良好的程序。
2012-10-05 cs.LO cs.PL
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report
通常，分布式系统的验证任务是通过计数器抽象来完成的。这种抽象有时可以通过模拟和互模拟来证明。在这项工作中，我们提供的逻辑基础，这种做法，通过一个专门设计的技术，二阶量词消去。我们的方法，一旦应用到规范的验证问题的参数化分布式系统，产生整数变量系统，准备好模型检查当前基于SMT的工具。我们证明了该方法的可行性与原型实现和第一次实验。
2017-12-05 cs.DC cs.LO cs.SE
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems
本文提出概率系统定量抽象的理论框架，结合范畴论、余代数和最优传输，通过伴随关系和定量逻辑实现抽象与实现的对偶性，为概率领域中的状态抽象和表示学习提供严格基础。
2026-03-12 cs.AI cs.LG cs.LO
On the distributed evaluation of recursive queries over graphs
诸如一阶逻辑（FO）和定点逻辑（FP）之类的逻辑形式主义非常适合以声明的方式表达分布式系统中所需的基本图形功能。我们表明，这些逻辑构成良好的抽象编程分布式系统作为一个整体，因为它们可以在一个完全分布式的方式进行评估，合理的复杂性上限。我们首先证明FO和FP可以用对数大小的消息的多项式数进行评估。然后，我们表明，（全球）的逻辑公式可以被翻译成规则程序描述的分布式系统的节点的本地行为，计算等价的结果。最后，我们介绍了这些逻辑，尽可能多地保留其分布式计算的本地片段，同时提供了丰富的网络功能的表达能力。我们证明，他们承认更严格的上限有界的消息数量有界的大小。最后，我们表明，本地片段的语义和复杂性被保存在本地一致的网络以及匿名网络，从而显示出所提出的本地逻辑形式主义的鲁棒性。
2009-04-21 cs.DC cs.LO
Denotational semantics of general store and polymorphism
本文首次提出结合卫递归与非直谓多态性的多态依赖类型理论指称语义，支持一般高阶引用和递归类型，并通过“逻辑关系即类型”的模态构造实现对有状态抽象数据类型的关系推理。
2023-04-12 cs.LO cs.PL
A declarative approach to specifying Paxos using three-valued modal fixpoint logic
本文提出三值模态不动点逻辑 Coalition Logic，将分布式算法表示为逻辑理论以声明式地规约和推导正确性，通过 Paxos 算法验证了其处理复杂系统的能力。
2026-10-23 cs.LO math.LO
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。
2001-01-15 cs.LO cs.PL
HMC: Verifying Functional Programs Using Abstract Interpreters
我们提出了Hindley-Milner-Cousots（HMC），一个算法，允许任何一阶命令式程序的过程间分析被用来验证类型化高阶函数程序的安全属性。HMC工作如下。首先，它利用函数程序的类型结构来生成一组逻辑精化约束，这些约束的满足意味着源程序的安全性。其次，它将逻辑精化约束转换成一个简单的一阶命令式程序，该程序是安全的，当且仅当约束是可满足的。因此，HMC一举使工具的不变生成，例如，基于抽象域、谓词抽象、反例引导的精化和Craig插值可以直接应用于以全自动的方式验证现代函数式语言的安全属性。我们已经实现了HMC，并描述了初步的实验结果，使用两个命令式检查器- ARMC和InterProc -来验证OCaml程序。因此，通过组成基于类型的推理在程序语法和基于状态的推理在抽象解释的基础上，HMC打开了大门，以现代程序设计语言编写的程序的自动验证。
2010-12-30 cs.LO cs.PL
Axe 'Em: Eliminating Spurious States with Induction Axioms
针对一阶逻辑（FOL）抽象建模中因语义差距导致的虚假状态问题，提出利用归纳公理精炼良基/有限域语义的方法，通过OSC片段归约证明可判定性，原型工具验证了其有效性。
2024-11-29 cs.LO cs.PL
