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
A Separation Logic for Concurrent Randomized Programs
我们提出了北极星，支持概率推理的并发分离逻辑。作为我们的逻辑的一部分，我们扩展了耦合的想法，这是最近的工作概率关系逻辑的基础，设置的程序与概率和非确定性的选择。为了演示北极星，我们验证了一个随机并发计数器算法和两级并发跳表的变体。我们所有的结果都在Coq中实现了机械化。
2018-11-21 cs.LO cs.PL
A Probabilistic Separation Logic
概率独立性是一个有用的概念，用于描述随机抽样的结果-所有概率语言中的基本操作-和用于推理随机变量组。然而，现有的验证方法处理独立性很差，如果有的话。我们提出了一个概率分离逻辑PSL，其中分离模型概率独立性。本文首先给出了一个新的聚束蕴涵逻辑（BI）的概率模型。然后，我们建立了一个程序逻辑的基础上，这些断言，并证明系统的可靠性。我们证明了我们的逻辑验证信息理论的安全性的密码结构的几个众所周知的任务，包括私人信息检索，不经意的传输，安全多方除了，和简单的不经意的RAM。我们的证明纯粹是根据高级属性进行推理的，比如独立性和一致性。
2020-07-17 cs.LO cs.PL
Independence and concurrent separation logic
一个组合的Petri网为基础的语义给出了一个简单的语言，允许指针操作和并行。然后，该模型被应用到给出一个概念的有效性并发分离逻辑，强调在这样的可靠性保证推理的过程-环境的二重性所作出的判断。合理性的并发分离逻辑的规则相对于这个定义的有效性。保留的Petri网模型的独立性信息，然后利用来表征的逻辑执行的并行进程的独立性。这表明允许能够改变原子动作的粒度的细化操作。
2008-03-19 cs.LO cs.PL
Automated Mutual Explicit Induction Proof in Separation Logic
本文提出了一个基于序列的演绎系统，用于利用数学归纳法自动证明分离逻辑中的蕴涵。我们的技术，称为相互显式归纳证明，是诺特归纳的一个实例。具体地说，我们提出了一种新的基于分离逻辑模型的良基关系的归纳原理，并遵循显式归纳方法将该原理实现为推理规则，从而可以很容易地集成到演绎系统中。我们还支持相互归纳，隐式归纳的一个自然特征，其中目标蕴涵和其他蕴涵在证明搜索过程中可以用作假设来证明对方。我们已经实现了一个原型证明器，并评估它的基准手工制作的蕴涵以及基准从分离逻辑竞争。
2016-09-06 cs.LO cs.PL
Relational Parametricity and Separation Logic
分离逻辑是霍尔逻辑的一个新的扩展，用于推理引用共享可变数据结构的程序。在本文中，我们提供了一个新的解释逻辑的程序设计语言具有更高的类型。我们的解释是基于雷诺的关系参数化，它提供了一个正式的连接之间的分离逻辑和数据抽象。
2008-05-15 cs.LO
Dynamic Separation Logic
本文提出分离逻辑的动态逻辑扩展，引入模态词覆盖五种基本指令，结合最弱前置条件演算与新型替代形式化，并在Coq中验证其可靠性与完备性。
2025-01-24 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Principles for Verification Tools: Separation Logic
一种原则性的程序验证和构造工具的设计方法适用于分离逻辑。控制流采用幂级数模型，卷积作为分离合取。泛型构造将资源幺半群提升为断言和谓词Transformer quantale。数据流由具体的存储/堆模型捕获。这些都与分离代数的可靠性证明。验证条件和转换律是通过谓词Transformer Quantale中的等式推理导出的。这种关注点的分离使得Isabelle/HOL证明中的实现简单且高度自动化。由此产生的工具是正确的建设，它是解释经典的链表反转的例子。
2014-10-16 cs.LO cs.PL
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
本文提出Trillium分离逻辑框架，通过内涵细化方法强化高阶并发与分布式分离逻辑，支持证明非平凡的安全性和活性属性，并分别实例化出Fairis和扩展Aneris以验证并发与分布式系统的活性及与TLA+模型的细化关系。
2024-08-22 cs.LO cs.PL
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
本文提出结果分离逻辑（OSL），一种同时支持正确性与不正确性推理的程序逻辑，通过框架规则和新的三归结符号执行算法，实现对具有计算效应程序的局部推理，推进了分离逻辑的合成性。
2024-03-13 cs.LO cs.PL
Internal Calculi for Separation Logics
我们提出了一个一般的方法来公理化分离逻辑与heaplet语义没有外部功能，如名词/标签。首先，我们为无量词分离逻辑设计了第一个（内部）希尔伯特式公理化。我们实例化的方法，通过引入一个新的分离逻辑的基本特征：它配备了分离合取，谓词LS，和一个自然的保护形式的一阶量化。我们应用我们的方法，其公理化。作为我们的方法的副产品，我们还建立了这个新的逻辑的确切的表达能力，我们显示其可满足性问题的P空间完备性。
2019-10-11 cs.LO
On Algebraic Abstractions for Concurrent Separation Logics
并发分离逻辑的特点是在并行组合和成帧时状态所有权的转移。支撑所有权转移的代数结构是部分交换幺半群（PCM）。现有的研究主要从逻辑的角度考虑所有权转移，而相对较少注意代数的考虑。本文利用保结构的部分函数（即，态射）之间的PCM，以及分离关系的相关概念。结构的态射是代数和范畴论中的标准概念，但在分离逻辑中还没有普遍使用过。分离关系是二元关系，它推广了不相交性，并描述了态射保持结构的输入。这两个抽象通过实现编写规范的简洁方式，通过提供在所有权转移下保留的线程状态的抽象视图，以及通过实现从现有PCM中构造新PCM的用户级构造，来促进验证。
2021-03-04 cs.LO cs.PL
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
定量分离逻辑（QSL）是分离逻辑（SL）的扩展，用于概率指针程序的验证。在QSL中，公式计算为实数而不是真值，例如，在给定的符号堆中，内存安全终止的概率。与\SL一样，使用QSL进行推理时的一个关键问题是\emph{entailment}：公式f是否包含另一个公式g？我们给出了从QSL中的蕴涵检查到SL中的蕴涵检查的一般性约简。这允许利用大量的SL研究来自动验证概率指针程序。我们分析了我们的方法的复杂性，并证明其适用性。特别是，我们得到的第一个可判定性结果，验证这些程序通过应用我们的减少到一个量化的扩展著名的符号堆片段的分离逻辑。
2022-01-27 cs.LO cs.PL
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
多处理器机器的程序通常执行忙等待同步。在本文中，我们向证明终止这类程序的第一步。我们近似（i）任意等待事件的突然程序终止和（ii）忙碌等待事件的忙碌等待被突然终止。我们提出了一个分离逻辑模块化验证终止（公平调度下）的程序，其中一些线程最终突然终止程序，和其他线程忙等待这种情况发生。
2020-07-21 cs.LO cs.PL
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
多处理器机器的程序通常执行忙等待同步。在本文中，我们向证明终止这类程序的第一步。我们近似（i）任意等待事件的突然程序终止和（ii）忙碌等待事件的忙碌等待被突然终止。我们提出了一个分离逻辑模块化验证终止（公平调度下）的程序，其中一些线程最终突然终止程序，和其他线程忙等待这种情况发生。
2020-10-16 cs.LO cs.PL
Separation Logic Modulo Theories
关于程序数据的逻辑推理通常需要处理堆结构以及标量数据类型。可满足性模块化理论（SMT）的最新进展已经提供了处理标量的有效程序，但它们缺乏对处理堆结构的任何支持。在本文中，我们提出了一种方法，集成了分离逻辑-一个突出的逻辑推理表段的堆-和SMT。我们遵循基于模型的方法，在SMT求解器和分离逻辑推理部分之间的堆单元之间传递别名。使用Z3求解器的实验评估表明，我们的方法可以有效地把工作的SMT处理堆结构的进步。这是分离逻辑与SMT理论相结合的第一个决策过程。
2013-03-11 cs.LO
Concurrent Separation Logic Meets Template Games
并发理论和程序设计语言语义学的一个古老梦想是揭示基本的同步机制，这些机制调节的情况与高阶程序的游戏语义和具有共享内存和锁的并发程序的霍尔逻辑一样不同。在本文中，我们建立了一个深刻的和意想不到的连接最近的两条工作线并发分离逻辑（CSL）和差分线性逻辑（DiLL）的模板游戏语义。由于这种联系，我们重新制定了纯粹的概念风格的模板游戏为迪尔的异步和交互式的解释CSL设计的梅利斯和Stefanesco。我们相信，分析揭示了一些重要的秘密解剖CSL，更具体地说，微妙的相互作用，分类性质，顺序组成，并行产品，错误和锁之间。
2020-05-09 cs.LO cs.PL
Strong-Separation Logic
大多数分离逻辑的自动验证器都以符号堆碎片为目标，不允许魔术棒运算符和经典布尔运算符应用于空间公式。这并不奇怪，因为对魔杖的支持很快导致了不可判定性，特别是当与归纳谓词结合用于数据结构的推理时。为了规避这些不可判定性的结果，我们建议分配一个更严格的语义分离合取。我们认为，由此产生的逻辑，强分离逻辑，可用于组合程序验证和双溯静态分析就像“标准”的分离逻辑，同时保持可判定的，即使在魔术棒和列表段谓词的存在下-功能的组合，导致undecidability假设标准的语义。
2021-03-11 cs.LO
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
除了前置条件和后置条件，最近的并行分离逻辑中的程序规范采用了一种资源的代数结构-状态转换系统的一种形式-来描述必须保留的基于状态的程序不变量，并记录允许的程序状态原子变化。在本文中，我们引入了一个新的概念，资源态射，即资源上的结构保持功能，并展示了如何有效地将其集成到分离逻辑，使用相关的概念态射特定的模拟。我们将态射和模拟应用于在一种资源下验证的程序，以使它们在另一种资源下运行，从而促进证明重用。
2019-10-15 cs.DC cs.LO cs.PL
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
本文提出Clutch，一种支持异步概率耦合的高阶概率关系分离逻辑，用于推理高阶程序的上下文精化与等价性，并在Coq中形式化验证。
2023-11-14 cs.LO cs.PL
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
我们提出了一个模型的子结构逻辑聚束的影响（BI），是适合于推理量子态。在我们的模型中，BI的分离合取描述了可分离的量子态。我们开发了一个程序逻辑，其中的前置条件和后置条件是描述量子态的BI公式-程序逻辑可以被看作是命令式量子程序的分离逻辑的对应物。我们练习逻辑证明量子一次性密码本和秘密共享的安全性，我们展示了如何使用程序逻辑来发现Google Cirq的变分量子算法（VQA）教程中的缺陷。
2021-01-30 cs.LO quant-ph
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
Permission-Based Separation Logic for Message-Passing Concurrency
基于分离逻辑和资源使用分析的思想，我们开发了消息传递并发程序的局部推理技术。我们扩展进程的权限资源，并定义了一个约简语义的扩展语言。这为解释消息传递并发的分离公式提供了基础。我们还定义了一个健全的证明系统，使我们能够推断满意度成分使用本地，分离为基础的推理。
2011-09-01 cs.LO
The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
在分离逻辑中用于检验指针程序的表段谓词非常适合于表示单链表的属性。我们研究了在完全无量词的分离逻辑中加入ls的效果，分离合取和蕴涵，这是由最近设计的新片段所激发的，在新片段中，所有这些成分都被无差别地使用，并且验证工具开始处理魔杖连接词。这是一个非常自然的扩展，迄今为止还没有被研究过。我们表明，没有分离的含义的限制，可以解决在多项式空间中使用适当的抽象记忆状态，而完整的扩展是不可判定的减少从一阶分离逻辑。当ls被添加时，从计算的角度也研究了逻辑和片段的许多变体，提供了关于将可达性谓词添加到无量词分离逻辑的许多结果。
2021-02-28 cs.LO
Refining Existential Properties in Separation Logic Analyses
在分离逻辑程序分析中，易处理性通常通过将不变量限制在有限的抽象域来实现。由于这个域不能变化，即使在底层逻辑中可以进行验证，信息丢失也可能导致失败。在本文中，我们提出了一种类似CEGAR的方法，用于检测虚假故障并通过细化抽象域来避免它们。我们的方法是面向发现存在的属性，例如“列表包含值x”。为了诊断故障，我们使用溯因推理，这是一种用于推断命令先决条件的技术。我们的方法从错误向后工作，识别因抽象而丢失的必要信息，并改进正向分析以避免错误。我们定义了几类存在属性的域，并在Redis，Azureus和FreeRTOS的案例研究中展示了它们的有效性。
2015-04-30 cs.LO cs.PL
Barriers in Concurrent Separation Logic: Now With Tool Support!
我们开发并证明了一个合理的并发分离逻辑的Pthreads风格的障碍。尽管Pthreads屏障在系统中被广泛使用，并且分离逻辑被广泛用于验证，但是还没有任何努力将两者结合起来。与锁和临界区不同，Pthreads屏障允许在多个线程之间同时进行资源重新分配，并且本质上是有状态的，导致逻辑设计及其可靠性证明的显着复杂性。我们展示了我们的逻辑可以应用到一个特定的示例程序中的模块化的方式。我们的校样在Coq进行机器检查。我们展示了一个程序验证工具集，自动应用逻辑规则，并履行相关的证明义务。
2012-04-19 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
Expressing the Behavior of Three Very Different Concurrent Systems by Using Natural Extensions of Separation Logic
分离逻辑是一种用于验证指针密集型代码的非经典逻辑。然而，在本文中，我们表明，分离逻辑，随着其自然的扩展，也可以作为一个规约语言的并发系统设计。为此，我们表达了三个非常不同的并发系统的行为：Subway，Stopwatch和2x2 Switch。Subway最初在LUSTRE中实现，Stopwatch在Esterel中实现，2x2 Switch在Bluespec中实现。
2009-11-11 cs.LO cs.SE
Resource separation in dynamic logic of propositional assignments
我们扩展了动态逻辑的命题分配，通过添加一个操作的并行组合，这是受分离逻辑。我们提供了一个公理化通过减少公理，从而建立决策。我们还证明了模型检验和可满足性问题的复杂性都停留在PSPACE中。
2021-04-30 cs.LO
Recursive Mutexes in Separation Logic
University of Illinois Chicago（伊利诺伊大学芝加哥分校）；Skylabs AI
本文研究了分离逻辑中递归互斥锁的规范方法，提出了一种统一处理多次获取和释放的规范方式，简化了客户端对锁状态的判断。
2026-01-30 cs.LO cs.PL
Separation Logic of Generic Resources via Sheafeology
针对现有分离逻辑理论无法统一构建多资源程序逻辑的问题，提出基于层范畴内部范畴逻辑的通用框架，实现支持一阶与分离联结词的通用资源分离逻辑，并通过多内存模型、随机变量实例验证。
2025-08-03 cs.LO
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
我们介绍堆自动机，一个形式主义的符号堆碎片的分离逻辑与用户定义的归纳谓词的鲁棒性自动推理。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。以前，这样的性质已经出现在分离逻辑文献的许多地方，但没有被系统地研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策程序。我们实现了我们的框架的原型，并取得了可喜的成果，所有上述的鲁棒性。此外，我们证明了堆自动机的适用性超出了鲁棒性。我们应用我们的算法框架的模型检验和蕴涵问题的符号堆分离逻辑。
2016-10-22 cs.LO
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
A Nominal Approach to Probabilistic Separation Logic
本文通过建立概率分离逻辑中基于测度论的分解与概率空间中基于乘积的分解之间的范畴等价，弥合了概率论与概率程序形式化推理之间的差距，并验证了先前设计决策。
2024-05-29 cs.LO cs.PL
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages
我们展示了如何给一个连贯的语义程序，以及指定的分离逻辑的一个版本的语言与更高的类型：理想化的algol扩展堆（但不可变的堆栈变量）。特别是，我们提供了简单的声音规则推导高阶框架规则，允许本地推理。
2006-11-03 cs.LO
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
本文提出用部分交换幺半群及其态射在分离逻辑中验证图算法，通过上下文局部化解决结构共享难题，并以Schorr-Waite算法和并查集验证其有效性。
2025-07-09 cs.LO cs.PL
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Nagasaki University（长崎大学）；Toho University（东邦大学）
本文通过将皮亚诺算术中的Pi-0-1公式翻译为仅包含直觉主义指向谓词、0和后继函数的分离逻辑小片段，证明了标准模型下算术公式的有效性等价于该片段中翻译公式的有效性，并由此得出该片段不可判定的新证明。
2026-05-22 cs.LO
Lilac: A Modal Separation Logic for Conditional Probability
本文提出分离逻辑 Lilac，用分离合取刻画概率独立性，并基于分解理论引入条件概率推理模态，成功形式化验证了依赖条件独立结构的加权采样算法。
2023-05-26 cs.LO cs.PL
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
本文研究了分离逻辑中证明机制的不完整性来源，并通过弱分离逻辑的完整性和非标准模型分析，揭示了证明失败的原因。
2025-12-04 cs.LO cs.PL
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
本文研究了$\exists^*\forall^*$语言中带有量词前缀的前向公式的分离合取和蕴涵无限制嵌套的分离逻辑在可能位置论域为可数无限或有限的情况下的可满足性问题.与带有未解释谓词和等式的一阶逻辑类似，我们称这个片段为伯奈斯-舍恩芬克尔-拉姆齐分离逻辑[BSR（SLk）]。我们表明，不同于在一阶逻辑中，（在）有限可满足性问题是不可判定的BSR（SLk），我们定义了两个非平凡的子集，这是可判定的有限和无限的可满足性，分别通过控制的范围内的普遍量化变量的出现分离的影响，以及后者的出现的极性。可判定性结果是通过分离连接词的受控消除获得的，描述为（i）将前束形式分离逻辑公式有效地翻译成少量\emph{test formulae}的组合，仅使用一阶连接词，随后（ii）将后者翻译成可均衡满足的一阶公式。
2018-02-16 cs.LO
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
带有归纳谓词的分离逻辑公式之间的蕴涵，也称为符号堆，已经被证明对于一大类归纳定义是可判定的。最近，提出了一个2-EXPTIME算法，并建立了一个EXPTIME硬界限，但没有精确的下限是已知的。在本文中，我们证明了决定谓词原子之间的蕴涵是2-EXPTIME困难的。证明是基于减少从指数空间有界交替图灵机的成员问题。
2020-04-16 cs.LO
Compositional Verification in Concurrent Separation Logic with Permissions Regions
本文提出带权限区域的 CSL-Perm 组合式验证系统，通过可推断框架规则残余堆的蕴涵过程实现线程与函数调用推理，并经 CoSl 工具验证其优势。
2025-10-06 cs.LO cs.PL
Formalizing and Verifying Decentralized Systems with Extended Concurrent Separation Logic
随着区块链等分布式账本技术的快速发展，去中心化技术正变得至关重要和无处不在。已经开发了许多分散式系统，通过这些技术以极大的可靠性和可靠性来解决安全和隐私问题。同时，分散系统的形式化和验证是保证设计正确性和实现安全性的关键。本文提出了一种新的方法，形式化和验证分散系统与一种扩展的并发分离逻辑。我们的逻辑扩展了标准的并发分离逻辑的新功能，包括通信封装，环境感知和节点级推理，增强了模块化和表达能力。此外，我们开发了统一性和兼容性的逻辑，以方便实现。此外，我们通过应用我们的逻辑来形式化和验证去中心化系统中的关键技术，包括共识机制和智能合约，来证明我们方法的有效性和多功能性。
2020-08-19 cs.DC cs.LO
A Complete Axiomatisation for Quantifier-Free Separation Logic
本文提出了首个针对无量化词分离逻辑的完全公理化，采用内部希尔伯特风格，分三部分处理核心公式、分离连接词消去及命题演算与布尔BI结构。
2021-08-09 cs.LO
Modular Verification of Heap Reachability Properties in Separation Logic
许多算法和数据结构的正确性依赖于可达性属性，即依赖于堆中对象之间引用链的存在。关于可达性的推理是困难的，主要有两个原因。首先，任何堆修改都可能影响无限数量的引用链，这会使模块化验证（特别是框架）复杂化。其次，SMT求解器不支持一般图的可达性，这阻碍了自动验证。本文提出了一种分离逻辑可达性的模块化描述和验证技术。对于每个方法，我们只在方法操作的堆的片段中本地指定可达性。一种新形式的可达性框架相对凸的子堆允许一个扩展的可达性属性从堆片段的调用者的更大的片段，使精确的过程模块化推理。我们的技术支持实际上重要的堆结构，即无环图与有界的出度以及（潜在的循环）图，每对节点之间最多有一个路径（模循环）。集成到分离逻辑允许我们以统一的方式推理可达性和其他属性，验证并发程序，并通过现有的分离逻辑验证器自动化我们的技术。我们证明，我们的验证技术是适合SMT为基础的验证编码到毒蛇验证基础设施的基准测试的例子。
2019-08-16 cs.LO cs.PL
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
New York University（纽约大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）
研究并发数据结构线性一致性中逻辑原子性规范与线性一致性的关系，证明Iris分离逻辑框架下能为线性一致数据结构导出逻辑原子性规范，将多种证明技术嵌入Iris并应用于多个队列实现，还建立相关联系并机械化结果。
2026-07-14 cs.LO cs.PL
A Separation Logic for Negative Dependence
关于基于散列的概率数据结构的形式化推理通常需要关于随机变量的推理，其中当一个变量变大时（例如散列到一个桶中的元素的数量），其他变量趋于变小（例如散列到其他桶中的元素的数量）。这是一个负相关的例子，它是概率独立性的推广，最近在算法设计和机器学习中发现了有趣的应用。尽管负相关对于概率数据结构的分析是有用的，但是现有的验证方法不能为随机化程序建立这种性质。为了填补这一空白，我们设计了LINA，概率分离逻辑推理负相关。继近年来概率分离逻辑利用分离合取推理随机变量的概率独立性之后，本文利用分离合取推理随机变量的负相关性。我们的断言逻辑具有两个分离的合取，一个用于独立，一个用于负依赖。本文将串蕴涵逻辑推广到支持多个分离连词，并给出了一个完善的证明系统。值得注意的是，用于分离合取的语义依赖于用于组合资源的非确定性操作，而不是部分操作。通过利用负依赖的闭包属性，我们的程序逻辑支持负依赖和单调操作的框架式规则。我们演示了如何LINA可以验证基于哈希的数据结构和balls-into-bin过程的概率属性。
2021-11-29 cs.LO cs.PL
Extending Concurrent Separation Logic to Enhance Modular Formalization
如今，许多基于大规模分布式系统的服务已经被开发出来，以提高人类生活的便利性。另一方面，由于这些系统的复杂性和嵌套性，确保其正确性和性能成为一个重大的挑战。虽然并发分离逻辑（CSL）通过指定系统并验证它们的正确性部分地解决了这个问题，但它面临着模块化问题。在本文中，我们提出了一个扩展的并发分离逻辑（ECSL），以解决CSL的模块化问题的时间扩展，通信扩展，环境扩展，嵌套扩展的支持。ECSL能够在从存储管理到体系结构和协议设计的不同抽象层次上对系统进行形式化，具有很强的模块性。在开发ECSL的过程中，坚持统一性和兼容性原则。
2020-07-27 cs.LO
Exact Separation Logic (Extended Version)
本文提出精确分离逻辑（ESL），一种既能验证所有终止行为又能确保结果可达的逻辑，首次实现 UX 逻辑的函数组合性，并探讨了抽象在 UX 推理中的作用。
2023-08-30 cs.LO cs.PL
A beginner guide to Iris, Coq and separation logic
本指南面向初学者，介绍使用 Iris 和 Coq 进行形式化验证，重点讲解示例、策略、分离逻辑，并全面覆盖相关工具，以帮助读者安全验证并发算法。
2025-01-23 cs.LO cs.PL
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
我们确定差异约束集约束（DBS），一个类比的差异约束算术约束集。DBS不仅可以表示集合约束，而且可以表示集合元素上的算术约束。我们将DBS集成到具有线性组合归纳谓词的分离逻辑中，获得其中可以指定线性数据结构的集合数据约束的逻辑。我们证明了这个逻辑的可满足性是可判定的。决策过程的一个关键步骤是计算DBS可定义的集合关系的传递闭包，为了捕获它，我们提出了一种扩展的量化集合约束与Presburger算术（RQSPA）。RQSPA的可满足性，然后证明是可判定的利用先进的自动机理论技术。
2018-11-02 cs.LO
An Asynchronous soundness theorem for concurrent separation logic
并发分离逻辑（CSL）是一种用于具有共享内存和锁的并发命令式程序的规范逻辑。在本文中，我们开发了一个并发和交互式帐户的异步游戏语义的启发逻辑。对于每个程序$C$，我们将一对异步转换系统$[C]_S$和$[C]_L$关联起来，它们描述了代码面对其环境或框架时的操作行为--在机器状态（$S$）和机器指令和锁（$L$）的级别上。然后，我们建立的每一个衍生树$π$的判断$Γ\vdash\{P\}C\{Q\}$定义了一个胜利和异步策略$[π]_{Sep}$相对于异步语义$[C]_S$和$[C]_L$。从这一点，我们推导出一个异步可靠性定理CSL，它指出，规范映射$\mathcal{L}:[C]_S\to[C]_L$从有状态语义$[C]_S$的无状态语义$[C]_L$满足一个基本的fibrational属性。我们主张，这提供了一个干净的和概念性的解释通常的CSL的可靠性定理，包括没有数据竞争。
2018-07-21 cs.LO cs.PL
