Strong-Separation Logic
大多数分离逻辑的自动验证器都以符号堆碎片为目标，不允许魔术棒运算符和经典布尔运算符应用于空间公式。这并不奇怪，因为对魔杖的支持很快导致了不可判定性，特别是当与归纳谓词结合用于数据结构的推理时。为了规避这些不可判定性的结果，我们建议分配一个更严格的语义分离合取。我们认为，由此产生的逻辑，强分离逻辑，可用于组合程序验证和双溯静态分析就像“标准”的分离逻辑，同时保持可判定的，即使在魔术棒和列表段谓词的存在下-功能的组合，导致undecidability假设标准的语义。
2021-03-11 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
Barriers in Concurrent Separation Logic: Now With Tool Support!
我们开发并证明了一个合理的并发分离逻辑的Pthreads风格的障碍。尽管Pthreads屏障在系统中被广泛使用，并且分离逻辑被广泛用于验证，但是还没有任何努力将两者结合起来。与锁和临界区不同，Pthreads屏障允许在多个线程之间同时进行资源重新分配，并且本质上是有状态的，导致逻辑设计及其可靠性证明的显着复杂性。我们展示了我们的逻辑可以应用到一个特定的示例程序中的模块化的方式。我们的校样在Coq进行机器检查。我们展示了一个程序验证工具集，自动应用逻辑规则，并履行相关的证明义务。
2012-04-19 cs.LO
Resource separation in dynamic logic of propositional assignments
我们扩展了动态逻辑的命题分配，通过添加一个操作的并行组合，这是受分离逻辑。我们提供了一个公理化通过减少公理，从而建立决策。我们还证明了模型检验和可满足性问题的复杂性都停留在PSPACE中。
2021-04-30 cs.LO
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
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages
我们展示了如何给一个连贯的语义程序，以及指定的分离逻辑的一个版本的语言与更高的类型：理想化的algol扩展堆（但不可变的堆栈变量）。特别是，我们提供了简单的声音规则推导高阶框架规则，允许本地推理。
2006-11-03 cs.LO
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Nagasaki University（长崎大学）；Toho University（东邦大学）
本文通过将皮亚诺算术中的Pi-0-1公式翻译为仅包含直觉主义指向谓词、0和后继函数的分离逻辑小片段，证明了标准模型下算术公式的有效性等价于该片段中翻译公式的有效性，并由此得出该片段不可判定的新证明。
2026-05-22 cs.LO
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
A Complete Axiomatisation for Quantifier-Free Separation Logic
本文提出了首个针对无量化词分离逻辑的完全公理化，采用内部希尔伯特风格，分三部分处理核心公式、分离连接词消去及命题演算与布尔BI结构。
2021-08-09 cs.LO
Extending Concurrent Separation Logic to Enhance Modular Formalization
如今，许多基于大规模分布式系统的服务已经被开发出来，以提高人类生活的便利性。另一方面，由于这些系统的复杂性和嵌套性，确保其正确性和性能成为一个重大的挑战。虽然并发分离逻辑（CSL）通过指定系统并验证它们的正确性部分地解决了这个问题，但它面临着模块化问题。在本文中，我们提出了一个扩展的并发分离逻辑（ECSL），以解决CSL的模块化问题的时间扩展，通信扩展，环境扩展，嵌套扩展的支持。ECSL能够在从存储管理到体系结构和协议设计的不同抽象层次上对系统进行形式化，具有很强的模块性。在开发ECSL的过程中，坚持统一性和兼容性原则。
2020-07-27 cs.LO
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
我们确定差异约束集约束（DBS），一个类比的差异约束算术约束集。DBS不仅可以表示集合约束，而且可以表示集合元素上的算术约束。我们将DBS集成到具有线性组合归纳谓词的分离逻辑中，获得其中可以指定线性数据结构的集合数据约束的逻辑。我们证明了这个逻辑的可满足性是可判定的。决策过程的一个关键步骤是计算DBS可定义的集合关系的传递闭包，为了捕获它，我们提出了一种扩展的量化集合约束与Presburger算术（RQSPA）。RQSPA的可满足性，然后证明是可判定的利用先进的自动机理论技术。
2018-11-02 cs.LO
Permission-Based Separation Logic for Multithreaded Java Programs
本文提出了一个程序逻辑推理多线程Java类程序的动态线程创建，线程连接和可重入对象监视器。该逻辑基于并发分离逻辑。它是并发分离逻辑到多线程类Java语言的第一个详细改编。程序逻辑将唯一的静态访问权限与每个堆位置相关联，以确保独占写入访问并排除数据竞争。通过部分权限支持并发读取。在线程启动、线程加入、初始监视器进入和最终监视器退出时，可以在线程之间传输数据。为了区分初始监视器进入和监视器重进入，辅助变量跟踪当前持有的监视器的多个集合。通过抽象谓词促进了数据抽象和行为子类型化，抽象谓词还用于表示监视器不变量、线程启动的先决条件和线程加入的后置条件。值参数化类型允许方便地捕获常见的强全局不变量，如静态对象所有权关系。的程序逻辑提出了一个模型语言与Java类和接口，程序逻辑的合理性被证明，并提出了一些说明性的例子。
2015-03-01 cs.LO
A Decision Procedure for Separation Logic in SMT
本文提出了一个完整的决策过程的整个量化器的分离逻辑（$\seplog$）的片段解释的heaplet的数据元素范围内的参数多排序（可能是无限的）域。该算法使用了理论的组合，并被用作一个专门的求解器内的DPLL（$T$）架构。在CVC 4 SMT求解器中实现了原型。初步评估表明，使用此程序作为一个更详细的定理证明SL与归纳谓词的积木，或作为后端的有界模型检查程序与低级别的指针和数据操作的可能性。
2016-05-19 cs.LO
Stone-Type Dualities for Separation Logics
本文系统建立了分离逻辑及其变体的Stone型对偶定理，统一处理BI、BBI及多种扩展逻辑，首次证明了DMBI等逻辑的可靠性与完备性，为资源语义提供了范畴论框架。
2019-03-13 cs.LO
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
本文研究了带计数的两变量一阶逻辑片段中的可定义性与分离问题，证明了在包含逆算子和名义时分离问题不可判定，而去除这些特征时其复杂度降为coNExpTime或2ExpTime完全，并指出可定义性问题通常可多项式归约至有效性问题。
2025-08-15 cs.LO
Incorrectness Separation Logic with Arrays and Pointer Arithmetic
本研究扩展了Incorrectness Separation Logic (ISL)以支持变长数组谓词和指针算术，并通过构造最弱后置条件证明了其相对完备性，确保了证明系统的可靠性。
2025-03-02 cs.LO
Sufficient Incorrectness Logic: SIL and Separation SIL
Meta Platforms, Inc.（Meta平台公司）
SIL是一种新的下界三元组基础程序逻辑，用于推理程序错误，通过区分导致错误的初始状态，提高错误检测的准确性。
2024-01-30 cs.LO
Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages
对于一类语言L，让PDL[L]是命题动态逻辑的扩展，它允许程序使用L语言而不仅仅是正则的。如果L包含非正则语言，则PDL[L]可以表示非正则属性，与纯PDL相反。对于规则的，可见的下推和确定性上下文无关的语言，各自的PDL的分离可以通过自动机理论技术来证明。然而，这些技术在自动机方面引入了非确定性。由于非确定性也是DCFL和CFL之间的区别，因此这些技术似乎不适合将PDL[DCFL]与PDL[CFL]分开。然而，这种分离是显示，但程序没有测试操作符。
2011-06-07 cs.LO
Completeness for a First-order Abstract Separation Logic
分离逻辑（SL）断言语言的定理证明的现有工作要么集中在抽象语义上，这在大多数程序验证应用中是不容易获得的，要么集中在具体模型上，这是不可能的。具体SL中的一个重要元素是指向谓词，它表示单例堆。带有指向谓词的SL已被证明是不可递归的。在本文中，我们开发了一个一阶SL，称为FOASL，与抽象版本的指向谓词。我们证明了FOASL是健全的和完整的抽象语义，其中标准SL语义是一个实例。我们还表明，一些推理原则，涉及点到谓词可以近似为FOASL理论，从而使我们的逻辑用于推理具体的程序验证问题。我们给出了一些例子理论，是健全的分离逻辑从文献中的不同变体，包括那些与雷诺兹的语义不兼容。在实验中，我们展示了我们的FOASL为基础的定理证明，这是能够处理大量的分离逻辑与堆语义，以及非标准的语义片段。
2016-08-24 cs.LO
Revisiting concurrent separation logic
提出了一种基于结构化操作语义（SOS）的并发分离逻辑（CSL）可靠性证明。我们建立在两个以前的证明，并开发新的辅助概念，以实现这一目标。一种使用指称语义（基于跟踪）。另一种是基于SOS，但只针对逻辑的一个片段（Disjoint CSL）获得，它不允许修改并发线程之间的共享变量。在这项工作中，我们解除了这样的限制，证明了健全的充分CSL就SOS。从而有助于开发能够保证实际并发程序正确性的工具。此外，考虑到我们使用SOS，这些工具可以很好地集成到编程环境中，甚至可以合并到编译器中。
2017-12-05 cs.LO
Two Results on Separation Logic With Theory Reasoning
本文给出了关于谓词符号为归纳定义的分离逻辑和理论推理中蕴涵问题的两个结果。首先，我们证明了在理论推理的情况下，对于树宽有界的规则，蕴涵问题是不可判定的。这一结果适用于许多理论，即使它们的表达能力很低。例如，它适用于具有后继函数或具有通常顺序的自然数。其次，我们证明了每个蕴涵问题都可以归结为一个蕴涵问题，不包含平等（无论是在公式中，也不是在递归规则定义的谓词符号的语义）。
2022-06-19 cs.LO
Deciding Entailments in Inductive Separation Logic with Tree Automata
具有归纳定义的分离逻辑（SL）是用于指定复杂递归数据结构的自然形式主义，用于操作此类结构的程序的组合验证。任何基于SL的自动验证过程的关键要素是蕴涵问题的可判定性。在这项工作中，我们减少了蕴涵问题的一个非平凡的子集SL描述树（和超越）的语言包含树自动机（TA）。我们的减少提供了严格的复杂性界限的问题，并表明在我们的片段的蕴涵是EXPTIME完成。出于实用的目的，我们利用自动机理论的最新进展，如包含检查非确定性TA避免明确的确定性。我们实现了我们的方法，并提出了有前途的初步实验结果。
2014-02-11 cs.LO
Relative Completeness of Incorrectness Separation Logic
针对操作堆的程序下近似问题，本研究聚焦于用于漏洞检测的不正确性分离逻辑（ISL），通过引入含变量别名的规范化方法计算最弱后置条件，结合允许无限析取的析取范式框架，证明了ISL的相对完备性。
2025-08-03 cs.LO
Towards Concurrent Quantitative Separation Logic
本文提出并发定量分离逻辑，将定量分离逻辑与并发分离逻辑结合，用于验证并发、指针和随机化程序实现后置条件的概率下界。
2024-09-30 cs.LO cs.PL
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
一个有效的蕴涵证明系统对于使用分离逻辑的组合验证是必不可少的。不幸的是，现有的决策程序要么缺乏表达能力，要么效率低下。例如，Smallfoot是一个有效的过程，但只适用于硬连接的列表和树。其他可以支持一般归纳谓词的过程在时间上呈指数级运行，因为它们的证明搜索需要回溯来处理结果中的析取。本文给出了一个在多项式时间内推导一般归纳谓词循环蕴涵证明的判定过程。我们的程序是高效的，不需要回溯;它使用规范化规则，有助于避免在后果中引入析取。此外，我们的可判定片段是足够的表达：它是基于组合谓词，可以捕获广泛的数据结构，包括排序和嵌套的列表段，跳跃列表与快速前进指针，和二叉搜索树。我们已经实现了一个原型工具的建议，并评估它的挑战性问题，从最近的分离逻辑竞争。实验结果证实了所提出的系统的效率。
2022-10-02 cs.LO
The Relationship Between Separation Logic and Implicit Dynamic Frames
分离逻辑是一种简洁的方法，用于指定操作动态分配的存储器的程序。部分受分离逻辑的启发，隐式动态框架最近被提出，旨在一阶工具支持。在本文中，我们精确地连接这两个逻辑的语义。我们定义了一个逻辑，其语法包含一个标准的分离逻辑，并作为子语法的隐式动态框架。我们为我们的逻辑定义了一个全堆语义，并且，对于分离逻辑子语法，证明它等价于标准的部分堆模型。为了定义一个语义，这两个子语法一致的工作，我们定义了一个新的概念，一个最小的状态扩展，它提供了一个不同的（但等效的）定义的语义分离逻辑的含义和魔术棒连接，同时也给出了一个合适的语义，这些连接在隐式动态框架。我们表明，我们得到的语义与现有的定义最弱的前条件语义的隐式动态框架片段。最后，我们表明，我们可以编码的分离逻辑片段，我们的逻辑到隐式动态框架片段，保持语义。对于工具通常支持的连接词，这表明分离逻辑可以忠实地编码在一阶自动验证工具（Chalice）中。
2012-07-29 cs.LO cs.PL
The Complexity of Prenex Separation Logic with One Selector
我们首先证明了具有$k\geq1$选择器域的分离逻辑（$\seplogk{k}$）的所有前向列公式的无限可满足性都可以化为有限可满足性。第二，我们表明，这需要的可判定性的有限和无限的可满足性问题的类前向公式的$\seplogk{1}$，减少到一阶理论的一元函数符号和一元谓词符号。我们还证明了复杂性不是初等的，通过减少从一元函数符号的一阶理论。最后证明了$\exists^*\forall^*$语言中带量词前缀的前趋$\seplogk{1}$公式的Bernays-Schönfinkel-Ramsey片段是\pspace -完全的.一个完整的（层次）分类的复杂性前束$\seplogk{1}$的定义，根据量词交替深度是一个悬而未决的问题。
2018-04-30 cs.LO
Trace Properties from Separation Logic Specifications
我们提出了一个正式的方法有关的抽象分离逻辑库规范的跟踪性能，他们执行客户端和库之间的交互。具有抽象谓词的分离逻辑强制执行资源规程，该资源规程约束何时以及如何在客户机和库之间进行调用。直观地说，这可以在交互跟踪上实施协议。这种直觉在分离逻辑界被广泛使用，但以前尚未被正式化。我们提供的就是这样一种形式化。我们的方法是基于使用包装器的仪器库代码，以诱导执行跟踪检查下的属性。通过考虑一个分离逻辑扩展与跟踪资源，我们证明了当一个库满足其分离逻辑规范，那么它的包装版本满足相同的规范，而且，保持跟踪属性作为一个不变量。因此，任何符合分离逻辑规范的客户端和库实现都将满足跟踪属性。
2017-02-09 cs.LO cs.PL
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
本文研究分离逻辑中带归纳定义谓词的蕴涵问题，针对P规则和loc-deterministic归纳规则片段给出多项式时间的可靠完备循环证明过程，并证明条件放宽后问题不可处理。
2025-07-11 cs.LO
An Outline of Separation Logic
分离逻辑是证明包含指针的程序的有效程序逻辑。用指针进行推理变得困难，特别是当由于指向给定单元位置的几个指针而产生混叠时。本文试图通过一些简单的例子来探讨别名问题，并引入分离合取的概念作为处理别名问题的工具，借助于一种具有四个指针操作命令的程序设计语言，引入分离逻辑作为标准霍尔逻辑的扩展。这些命令执行通常的堆操作，如查找、更新、分配和释放。以半形式化的形式给出了新的分离逻辑断言和公理集。最后通过实例说明了新断言和公理的独特性。最后给出了利用分离逻辑公理对实际程序的证明。
2017-03-31 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
Flexible Refinement Proofs in Separation Logic
Department of Computer Science, ETH Zurich（苏黎世联邦理工学院计算机科学系）
本文提出了一种基于分离逻辑的新型细化技术，通过松散耦合抽象模型与具体实现，支持多种程序结构和逻辑，提升并发实现的效率与灵活性。
2021-10-26 cs.LO
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
An Algebraic Glimpse at Bunched Implications and Separation Logic
我们从小野宏明的代数方法的启发，子结构逻辑的角度概述了集束蕴涵（BI）和分离逻辑（SL）的逻辑。我们提出广义BI代数（GBI代数）作为一个共同的框架，代数产生通过“声明性资源阅读”，直觉主义的关系代数和箭头逻辑和分配Lambek演算的直觉主义的含义。除了现有的BI模型（特别是堆模型和效果代数），我们还涵盖了模型所产生的弱化关系，形式语言或更细粒度的治疗标记树和半结构化数据。在简要讨论了GBI的子簇格之后，我们沿着Esakia和Priestley的思路给出了GBI的一个合适的对偶，并在Galatos和Jipsen的剩余标架的背景下给出了割消的代数证明.我们还展示了如何代数方法允许通用的结果的可判定性，积极和消极的。在本文的最后一部分，我们轻轻地介绍了一些理论背后的最先进的工具，最终与代数和证明理论介绍（双）溯因。
2018-09-25 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
A Game Semantics of Concurrent Separation Logic
在本文中，我们发展了一个博弈论的帐户并发分离逻辑。对于代码在环境中的每一个执行轨迹，我们都关联了一个规范游戏，其中夏娃为代码而亚当为环境而游戏。Eve和Adam的目的是将执行跟踪的每个中间机器状态分解为三部分：一部分用于代码，一部分用于环境，一部分用于可用的共享资源。我们建立健全的并发分离逻辑解释每一个派生树的逻辑作为一个获胜的策略，这个规范的游戏。
2017-10-06 cs.LO cs.PL
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
灯塔项目，如CompCert，seL 4，IronFleet和DeepSpec已经证明，通过在抽象系统规范和可执行实现之间建立细化关系，可以对整个系统进行全面验证。然而，现有的方法施加严重的限制，无论是抽象的系统规范，由于其有限的表现力或多功能性，或可执行代码，由于其依赖于次优的代码提取或无表现力的程序逻辑。我们提出了一种新的方法，结合了组成细化的抽象，基于事件的模型的分布式系统与验证的成熟的程序代码，使用表达分离逻辑，支持功能的现实程序设计语言，如可变堆数据结构和并发。我们的工作的主要技术贡献是一个正式的框架，健全的基于事件的系统模型，程序规范的分离逻辑，这样的成功验证建立了一个细化模型和代码之间的关系。我们在Isabelle/HOL中正式定义了我们的框架Igloo。我们的框架，使现有的程序验证器的协议开发工具的良好组合。我们报告的三个案例研究，领导人选举协议，复制协议，和安全协议，我们完善正式的要求到程序规范（在伊莎贝尔/HOL），我们在Java和Python中实现，并证明正确使用VeriFast和Nagini工具。
2020-10-09 cs.LO
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
我们提出了定量分离逻辑（$\mathsf{QSL}$）。与经典的分离逻辑相反，$\mathsf{QSL}$采用计算为实数的量，而不是计算为布尔值的谓词。将经典分离逻辑的连接词分离合取和分离蕴涵从谓词提升为量。这个扩展是保守的：这两个连接词是向后兼容的经典类似物，并遵守相同的法律，例如肯定前件，伴随性等。此外，我们开发了一个最弱的前提演算概率指针程序的定量推理$\mathsf{QSL}$。这种演算是Reynolds的堆操作程序的分离逻辑和Kozen/ McIver和Morgan的概率程序的最弱预期望的保守扩展。可靠性证明相对于一个基于马尔可夫决策过程的操作语义。我们的演算保留了O 'Hearn的框架规则，使本地推理。我们证明，我们的演算能够推理数量，如终止与空堆的概率，达到一定的数组排列的概率，或列表的预期长度。
2018-11-26 cs.LO cs.PL
The Tree Width of Separation Logic with Recursive Definitions
分离逻辑是一种广泛使用的形式主义，用于描述动态分配的链接数据结构，如列表，树等的逻辑的各个片段的可判定性状态构成了一个长期存在的开放问题。目前的结果报告的技术，以确定满足性和有效性的蕴涵分离逻辑（S）的列表（可能与数据）。在本文中，我们建立了一个更一般的可判定性结果。我们证明了任何使用较一般的递归定义谓词的分离逻辑公式都是可判定的可满足性，而且这些公式之间的蕴涵也是可判定的有效性.这些谓词足够通用，可以定义（双）链表、树和比树更通用的结构，比如叶子被链接在一个链表中的树。可判定性证明是通过将一元二阶逻辑在有界树宽度的图上的可判定性归约来实现的。
2013-03-30 cs.FL cs.LO
Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation
本文提出将带 Gospel 注释的 OCaml 程序翻译为中间验证语言 Viper，通过扩展 Gospel 支持分离逻辑特性，为 Cameleer 扩展新后端以验证依赖堆的 OCaml 程序。
2024-12-19 cs.LO
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
有界验证已被证明是有用的，以检测错误，并增加在程序的正确性的信心。与无界验证相比，通过（有界）内联进行调用和通过（有界）展开进行循环的推理不需要方法规范和循环不变式，因此将注释开销降低到最低限度，即要验证的属性的规范。对于基于传统程序逻辑的验证器，通过内联（和展开）来保存验证：成功的程序w.r.t.某些注释意味着内联程序的成功验证。也就是说，在内联程序中检测到的任何错误都揭示了原始程序中的真正错误。但是，这个基本属性可能不适用于自动分离逻辑验证器，如Caper、GRASShopper、RefinedC、Steel、VeriFast和基于Viper的验证器。在这种情况下，内联通常会更改方法执行所拥有的资源，这可能会影响自动证明搜索算法并引入虚假错误。在本文中，我们提出了第一种技术，验证保持内联自动分离逻辑验证。我们确定了一个语义条件的程序，并证明在Isabelle/HOL，它确保了验证保持内联的最先进的自动分离逻辑验证。我们还证明了一个双重结果：成功验证的内联程序，确保有方法和循环注释，使验证的原始程序有界执行。为了自动检查我们的语义条件，我们提出了两个近似，可以检查语法和程序验证器，分别。我们实现这些检查毒蛇，并证明他们是有效的非平凡的例子，从不同的验证。
2023-03-13 cs.LO
Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version)
针对并发验证中临时共享状态的处理难题，提出Iris分离逻辑库Leaf，通过引入guarding算子实现模块化抽象，支持用户验证新共享策略，并以读写锁和哈希表案例验证了其有效性。
2023-09-09 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
Deciding Boolean Separation Logic via Small Models (Technical Report)
本文提出一种基于小模型边界优化和SMT翻译的分离逻辑判定过程，支持复杂布尔结构与常见链表变体，在符号堆片段上具有竞争力并能处理此前无判定过程的公式。
2024-03-27 cs.LO
On the Complexity of Pointer Arithmetic in Separation Logic (an extended version)
我们研究了在分离逻辑中增加指针运算的复杂性后果。具体来说，我们研究扩展的点到片段的符号堆分离逻辑与各种形式的Presburger算术约束。最重要的是，我们发现，即使在最小的情况下，当我们只允许简单的“差异约束”的合取，（x ′ \leq x+k）其中k是整数，多项式时间可判定性已经是不可能的：可满足性成为NP完全，无量词蕴涵成为CoNP完全蕴涵，量化蕴涵成为P2完全蕴涵（P2是多项式时间层次中的第二类）事实上，我们证明了上界是相同的，P2，即使对于全指针算术，但具有固定的指针偏移量，其中我们允许初等公式的任何布尔组合（x '= x+ k 0），（x' \leq x+ k 0）和（x'<x+ k 0），并且，除了指向公式之外，我们允许长度由k 0限定的数组的空间公式和长度由k 0限定的列表等，其中k 0是固定整数。然而，如果我们允许一种更有表现力的指针算术形式-即任意指针和上的基本公式的任意布尔组合-那么对于可满足性和无量化器蕴涵来说，复杂度的增加相对温和：它们仍然分别是NP-完全和coNP-完全的，并且对于量化蕴涵来说，复杂度似乎急剧增加。
2018-03-08 cs.LO
Formalizing and Verifying Decentralized Systems with Extended Concurrent Separation Logic
随着区块链等分布式账本技术的快速发展，去中心化技术正变得至关重要和无处不在。已经开发了许多分散式系统，通过这些技术以极大的可靠性和可靠性来解决安全和隐私问题。同时，分散系统的形式化和验证是保证设计正确性和实现安全性的关键。本文提出了一种新的方法，形式化和验证分散系统与一种扩展的并发分离逻辑。我们的逻辑扩展了标准的并发分离逻辑的新功能，包括通信封装，环境感知和节点级推理，增强了模块化和表达能力。此外，我们开发了统一性和兼容性的逻辑，以方便实现。此外，我们通过应用我们的逻辑来形式化和验证去中心化系统中的关键技术，包括共识机制和智能合约，来证明我们方法的有效性和多功能性。
2020-08-19 cs.DC cs.LO
