On the construction of multi-valued concurrent dynamic logic
动态逻辑是对命令式程序进行推理的强大框架。引入了一个带有并发操作符的扩展[18]来形式化并行运行的程序。在另一个方向上，其他作者提出了一个系统的方法来生成多值命题动态逻辑来推理加权程序[14]。本文介绍了这两个框架相结合，在并发计算中引入不确定性的第一步。在开发的框架中，权重被分配给并行执行的每个分支，导致模糊编程范式固有的（可能的）非对称并行性[21，2]。通过采用这样的方法，得到了一族逻辑，称为多值并发命题动态逻辑（CGDL（A）），参数上的动作格A指定的“权重”的概念分配给程序执行。此外，还讨论了CPDL中某些公理在新的生成逻辑族中的有效性。
2019-11-01 cs.LO
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
本研究提出一种嵌入简单类型高阶逻辑的并发命令式程序建模、验证与转换框架，可支持对交错计算命令式程序模型性质的可靠结构化推理，并通过Peterson互斥算法案例验证了其适用性。
2024-07-14 cs.LO
An Epistemic Perspective on Consistency of Concurrent Computations
并发计算的一致性属性，例如，顺序一致性、可线性化性或最终一致性对于设计正确的并发算法是必不可少的。在本文中，我们提出了一个逻辑形式化的一致性属性，是基于一个标准的逻辑知识。我们的形式化提供了一个声明性的角度来看，什么是一致性要求，并提供了一些有趣的统一见解不同的外观属性。
2013-05-10 cs.LO
A Concurrent Constraint Programming Interpretation of Access Permissions
面向对象（OO）程序设计语言中的最近趋势是使用Access对象（AP）作为控制程序的并发执行的抽象。AP源代码注释的使用定义了一个协议，指定对象引用如何访问对象的可变状态。虽然AP的使用简化了编写并发代码的任务，但不系统地使用它们可能会导致一些微妙的问题。本文提出了一个声明性解释的AP线性并发约束程序（LCC）。我们将AP表示为约束（即，逻辑中的公式），其蕴涵关系对AP的转换规则进行建模。此外，我们使用LCC中的流程来模拟AP所施加的依赖关系，从而使其在程序中的流的忠实表示。我们利用Girard直觉线性逻辑（ILL）中的公式对LCC过程的解释来验证AP程序的相关性质。属性包括死锁检测、程序正确性（程序是否遵守其AP规范）和方法并发运行的能力。通过依赖于ILL的聚焦纪律，我们提供了一个复杂性的措施，证明上述属性。我们的验证技术的有效性证明，通过实施凹室工具，包括一个动画和验证。前者执行lcc模型，观察AP的流程，并快速找到AP与实现的不一致之处。后者是一个基于ILL的自动定理证明器。这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2018-02-13 cs.LO
Restructuring a concurrent refinement algebra
本文重构支持 rely/guarantee 推理的并发精化代数，统一其 quantale/biquantale 结构并强化交换与分配性质，且在 Isabelle/HOL 中实现。
2024-05-09 cs.LO
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
并发Kleene代数是一个优雅的工具，用于并发程序的等式推理。CKA缺少的并发程序的一个重要特性是限制合法交织的能力。为了弥补这一点，我们扩展了标准模型的CKA，即pomsets，一个新的功能，所谓的盒子，它可以指定该系统的一部分是保护免受外界干扰。我们研究了这个新模型的代数性质。CKA的另一个缺点是用于表达程序属性的语言与用于表达程序本身的语言相同。对于实际目的来说，这通常限制太多。我们提供了一个逻辑，“pomset逻辑”，这是一个断言语言，用于指定这些属性，并解释pomset与框。与其他方法相比，这种逻辑不是基于状态的，而是表征程序的运行时行为。我们开发的基本元理论的pomset逻辑和CKA之间的关系，包括框架规则，以支持本地推理，并说明这种关系与简单的例子。
2020-05-06 cs.LO
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
Reachability and Termination Analysis of Concurrent Quantum Programs
我们介绍了并发量子程序的马尔可夫链模型。该模型是Hart，Sharir和Pnueli概率并发程序的量子推广。通过分析并发量子程序的可达空间、一致重复可达空间和可终止性的数学结构，给出了它们的一些特征。在此基础上，给出了计算可达空间、一致重复可达空间和判定终止性的算法。
2012-06-09 cs.LO quant-ph
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
程序部分的综合对于并发系统是非常有用的。然而，大多数合成方法不支持常见的设计任务，如修改单个过程而无需重新合成或验证整个系统。假设保证综合（AGS）提供了对系统部分修改的鲁棒性，但迄今为止一直局限于完美的信息设置。这意味着局部变量不能对其他过程隐藏，这使得合成结果繁琐甚至不可能实现。我们解决了这个缺点，定义AGS在部分信息设置。我们分析了在不同的设置的复杂性和可判定性，表明该问题具有很高的最坏情况下的复杂性，在许多有趣的情况下是不可判定的。基于这些观察，我们提出了一个务实的算法的基础上有界综合，并证明了它的实际适用性的几个例子。
2014-11-17 cs.LO
Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs
我们提出了一个框架，需要一个并发程序组成的不同步的进程，随着其全球并发行为的时间规范，并自动生成一个并发程序同步，确保正确的全球行为。我们的方法支持有限状态的并发程序组成的进程，可能有本地和共享变量，可能是直线或分支程序，可能正在进行或终止，并可能有程序初始化或用户初始化的变量。规约语言是命题计算树逻辑（CTL）的扩展，其使得能够容易地对控制和数据变量的安全性和活性属性进行规约。该框架还支持在不同的抽象和粒度级别上合成同步。
2012-07-04 cs.LO cs.PL
Proving correctness of Timed Concurrent Constraint Programs
提出了一种用于时间并发约束程序正确性推理的时态逻辑。这种逻辑是基于模态，它允许人们指定一个过程产生什么作为对其环境输入的反应。这些模态提供了一个假设/承诺风格的规范，允许一个健全的和完整的组合公理化的反应行为的定时并发约束程序。
2002-08-28 cs.LO cs.PL
Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications
我们提出了一个易于处理的方法合成任意大的并发程序，共享内存模型与常见的硬件可用的原语，如原子寄存器，比较和交换，加载链接/存储条件等，我们合成的程序是动态的：新的进程可以创建和添加在运行时，所以我们的程序是不有限的状态，一般。尽管如此，我们成功地利用自动合成和模型检查方法的命题时序逻辑的基础上。我们的方法在算法上是有效的，在任何时候都是“活”的组件进程（程序）的数量的复杂性多项式。我们的方法不显式地构造所有进程的自动机理论产品，从而避免了\intr{state explosion}。相反，对于每一对相互作用的过程，我们的方法构建了一个自动机理论产品（\intr{pair-machine}），它体现了这两个过程的所有可能的相互作用。从每个配对机器，我们可以合成一个正确的\intr{pair-program}，它根据需要协调两个相关的过程。我们允许这样的配对程序在运行时动态添加。然后，它们与当前活动的配对程序“合取组合”，以重新合成程序，因为它在添加新的配对程序后产生。因此，我们能够在运行时添加新的行为，从而满足新的属性。我们建立了一个“大模型”定理，该定理表明合成的大程序继承了配对程序的正确性属性。
2008-01-10 cs.LO
Logical Concurrency Control from Sequential Proofs
我们感兴趣的是识别和执行并发程序的隔离要求，即，确保程序满足其规范的并发控制。本文的论点是，这可以从顺序证明开始系统地进行，即，在没有并发交织的情况下证明程序的正确性。我们说明我们的论文提出了一个解决方案的问题，使一个顺序库线程安全的并发客户端。我们考虑一个顺序库注释断言以及证明这些断言在顺序执行。我们展示了如何使用证明来导出并发控制，以确保库方法的任何执行在由并发客户端调用时满足相同的断言。我们还提出了一个扩展，以保证库方法是线性化或原子。
2011-09-01 cs.LO cs.PL cs.SE
A Separation Logic for Concurrent Randomized Programs
我们提出了北极星，支持概率推理的并发分离逻辑。作为我们的逻辑的一部分，我们扩展了耦合的想法，这是最近的工作概率关系逻辑的基础，设置的程序与概率和非确定性的选择。为了演示北极星，我们验证了一个随机并发计数器算法和两级并发跳表的变体。我们所有的结果都在Coq中实现了机械化。
2018-11-21 cs.LO cs.PL
VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)
证明并发软件不会泄露其秘密的方法至少在过去的四十年里一直是一个活跃的研究课题。尽管开展了一系列令人印象深刻的工作，但目前的情况仍然非常不令人满意。使用当代的组合证明方法，人们被迫在表达性（推理各种安全策略的能力）和精确性（推理复杂线程交互和程序行为的能力）之间做出选择。实现这两个是必不可少的，我们认为，需要一种新的风格的组合推理。我们提出了VERONICA，第一个程序逻辑证明并发程序信息流安全，支持组合，高精度的推理范围广泛的安全策略和程序行为（例如，表达去分类，值相关的分类，秘密相关的分支）。同样重要的是，VERONICA体现了一种新的方法，用于工程这样的逻辑，可以在其他地方重用，称为解耦功能正确性（DFC）。DFC导致了一个简单而清晰的逻辑，即使在实现这种前所未有的功能组合的同时。我们证明了VERONICA的优点和多功能性，通过验证一系列的例子程序，超出了以前的方法。
2020-01-30 cs.LO
Compositional Reasoning for Shared-variable Concurrent Programs
并发系统的可扩展和自动化形式化验证一直是一个迫切的需求。在本文中，我们提出了一个验证框架，以支持自动组合推理的并发程序共享变量。我们的框架模型并发程序作为简洁的自动机，并支持多个重要属性的验证。简洁自动机的安全性验证和仿真是并行组合的，简洁自动机的安全性在精化过程中保持不变。我们以自动化的方式从无限状态并发程序中生成简洁的自动机。此外，我们提出了第一个自动化的方法来检查可靠保证无限状态并发程序之间的模拟。我们已经将我们的算法原型化，并将我们的工具应用于多个改进的验证。
2018-03-26 cs.FL cs.LO cs.SE
Concurrent Gaussian elimination
在支持提取并发程序的半构造性逻辑系统中，基于高斯消元的构造性证明，提取了一个求逆非奇异实值矩阵的程序，并利用并发机制实现高效选主元。
2023-05-17 cs.LO
Concurrent bisimulation algorithm
并发系统的粗互模拟发现问题在并发系统的形式化分析中起着重要的作用。例如，解决这个问题可以比较不同过程的行为或验证规范。因此，本文提出了一种有效的并发互模拟算法。它是基于顺序Paige和Tarjan算法和状态签名的概念。最初的解决方案遵循Hopcroft的原则“处理较小的一半”。所提出的算法使用其广义版本“处理所有，但最大的一个”更适合并发和并行应用程序。所实现的运行时间与最知名的顺序和并发解决方案相当。在工作的最后，进行了测试的结果。文中还讨论了最优算法运行时间的下界问题。
2014-01-10 cs.DC cs.LO
A Framework for Concurrent Imperative Programming
该框架提供了一个通用的并发命令式编程模型。程序被建模为形式语言，并发性被建模为交织（或混洗）运算符。这产生了一个简单而优雅的程序代数。该框架支持Dinsdale-Young等人的视图程序逻辑，它概括了各种类型系统和程序正确性的分离逻辑方法。它还验证了熟悉的操作演算在小步和大步的味道。程序逻辑相对于操作规则的一致性是直接建立的，并且不使用推导上的归纳。事实上，整个框架只使用简单的数学。参数化的状态，视图和基本命令，它可以实例化为各种具体的语言和设置。
2012-09-10 cs.LO cs.PL
Encoding fairness in a synchronous concurrent program algebra: extended version with proofs
并发程序精化代数为支持共享内存并发程序的组合式机械推理提供了一个合适的基础，例如，它支持Jones的依赖/保证方法。该代数利用了Aczel的并发跟踪模型和Milner的SCCS相似的同步并行操作符。本文着眼于在程序代数中定义一种形式的公平性。编码允许一个原因，公平执行一个单独的进程，以及定义公平并行的基本并行运算符，其中没有公平性的假设。建立了支持公平性和公平并行的代数理论。
2018-05-04 cs.DC cs.LO
Owicki--Gries Logic for Timestamp Semantics
STAIR Lab, Chiba Institute of Technology（千叶工业大学）
本文提出了一种基于时间戳语义的并发程序逻辑，通过引入新的非干扰概念，解决了弱内存模型下存储指令效果延迟的问题。
2026-02-16 cs.LO
On the Expressivity of Typed Concurrent Calculi
本论文全面探究支撑类型化编程语言的形式化计算模型，聚焦函数式与并发程序演算，指出其为程序语义评估及相关分析、验证技术开发提供严谨框架，为含附录的完整版论文。
2024-08-15 cs.LO cs.PL
Abstract Interpretation of Temporal Concurrent Constraint Programs
时间并发约束编程（Timed Concurrent Constraint Programming，tcc）是一种声明式的并发模型，提供了一种用于指定反应式系统（reactive systems）的逻辑，即与环境持续交互的系统。通用tcc形式主义（utcc）是tcc的扩展，具有表示移动性的能力。这里，移动性被理解为私有名称的通信，如通常针对移动系统和安全协议所做的。在本文中，我们考虑了tcc的指称语义，并将其扩展为基于约束序列上的闭包运算符的utcc的“收集”语义。依靠这种语义，我们形式化了一个通用框架的数据流分析的tcc和utcc程序的抽象解释技术。我们提出的具体和抽象语义是组合的，从而使我们能够减少数据流分析的复杂性。我们表明，我们的方法是健全的和参数的抽象域。因此，可以通过实例化框架来执行不同的分析。我们说明了如何可以重用抽象域先前定义的逻辑编程执行，例如，接地分析TCC程序。我们展示了这种分析在反应系统的背景下的适用性。此外，我们还利用抽象语义来展示一个安全协议中的秘密缺陷。我们还展示了如何有可能作出分析，这可能表明，tcc程序暂停免费。这对于多种用途都很有用，例如优化编译或调试。
2013-12-09 cs.LO
Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style
本文提出了一种基于 Rely-Guarantee 风格的共享内存并发算法精化理论，通过广谱语言编码规约条件并推导出综合精化定律，支持细粒度并发且在 Isabelle/HOL 中完成形式化证明。
2023-09-09 cs.LO
Denotational Semantics for Probabilistic and Concurrent Programs
本文针对兼具概率动作与并行组合的命令式程序，提出具有良好域论性质的指称模型，并通过两个适当性定理证明其统一涵盖并发与概率非确定语义。
2025-06-07 cs.LO cs.PL
Bilateral Proofs of Safety and Progress Properties of Concurrent Programs
本文提出了并发程序的可组合规格说明的一种理论，它允许：（1）对给定规格说明的程序代码进行验证;（2）组合组件的规格说明以产生程序的规格说明。该规范包括在程序执行结束时（如果执行终止）保持的终端属性和在整个执行过程中保持的永久属性。我们设计（1）证明技术的验证，和（2）组合规则，以获得规格的程序，从它的组件。我们利用组件的终端属性导出永久的性质的程序，反之亦然。因此，这种证明策略被称为双边的。该理论的组成方面是很重要的，在组装程序的组件，其中一些源代码可能是不可用的，因为越来越多的情况下，跨供应商的程序集成。
2017-04-05 cs.LO cs.PL
Syntactic Regions for Concurrent Programs
为了更好地理解程序的状态空间，为了使其验证更易于处理，引入了基于有向拓扑空间的模型，允许考虑执行轨迹之间的等价性，以及将执行的特征（例如死锁的存在）转化为几何情况。在这方面，许多算法被引入，基于描述的几何模型作为区域组成的工会的矩形。我们在这里解释说，这些结构实际上可以直接在程序的语法上执行，从而导致更自然，更容易实现的表示。为了做到这一点，我们从观察开始，在程序中的位置可以被描述为程序的部分探索。操作语义在位置上引入了偏序，并且区域可以被定义为结果偏序集中的区间的形式并集。然后，我们研究这些地区的结构，并表明，在合理的条件下，他们形成一个布尔代数，并承认在范式（这对应于覆盖一个空间的最大间隔）表示，从而支持建设所需的研究计划的目的。这里涉及的所有操作都给出了明确的算法描述。
2021-12-28 cs.LO
Automated Verification of Reactive and Concurrent Programs by Calculation
反应式程序将传统的顺序编程结构与原语相结合，以允许与其他并发代理进行通信。它们在现代应用中无处不在，从组件系统和Web服务到网络物理系统和自主机器人。在本文中，我们提出了一个代数验证策略的并发反应式程序，与一个大的或无限的状态空间。我们定义了新的运营商来描述相互作用和状态更新，以及相关的方程理论。有了这个，我们可以计算一个反应式程序的指称语义，从而促进自动证明。值得注意的是，我们的推理支持迭代程序与反应不变量，Kleene代数的基础上，并行组成。我们通过验证反应缓冲区来说明我们的策略。我们的法律和战略是机械化的伊莎贝尔/UTP，我们的霍尔和他的统一编程理论（UTP）框架的实施，提供健全的保证和实际的验证支持。
2021-04-12 cs.LO cs.PL
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
2025-08-07 cs.LO cs.PL
A Concurrent Program Logic with a Future and History
细粒度的乐观并发程序仍然是一个悬而未决的问题。现代程序逻辑提供了抽象机制和组合推理原则来处理固有的复杂性。然而，它们的使用主要局限于纸张和纸张或机械化的证明。我们设计了一个新的分离逻辑，面向缺乏自动化。虽然本地推理是众所周知的自动化是至关重要的，我们是第一个展示如何保持这种局部性（i）推理归纳属性，而不需要幽灵代码，和（ii）推理计算历史的事后诸葛亮。我们在一个工具中实现了我们的新逻辑，并使用它来自动验证具有挑战性的并发搜索结构，这些结构需要归纳属性和事后推理，例如Harris集。
2022-11-11 cs.LO cs.PL
The Singularity Theory of Concurrent Programs: A Topological Characterization and Detection of Deadlocks and Livelocks
该研究提出并发程序分析的奇点理论范式，通过分支拓扑空间建模程序执行，用代数拓扑不变量检测死锁与活锁，为并发验证提供新的拓扑基础。
2025-10-29 cs.DC cs.LO cs.PL
Some Challenges of Specifying Concurrent Program Components
本文的目的是解决一些挑战，正式指定组件的共享内存并发程序。重点是提供组件的抽象规范，该规范既适合于组件的客户端使用，又适合于作为细化组件实现的起点。我们提出了一些设计规范的方法，研究适合不同背景的不同形式。我们检查处理原子性的访问数据结构，阻塞操作和进度属性，以及可能会失败，需要重试的事务操作。
2018-10-23 cs.LO cs.PL
Extracting total Amb programs from proofs
我们提出了一个逻辑系统CFP（并发不动点逻辑），从它的证明可以提取不确定性和并发的程序，可证明的全部和正确的证明公式。CFP是一个直觉一阶逻辑，具有由两个命题算子A扩展的归纳和上归纳定义，||B（限制，加强蕴涵B -> A）和$\ddownarrow(A)$（完全并发）。提取的目标是一个具有构造函数和由构造函数Amb（用于麦卡锡的amb）扩展的递归的λ演算，它被解释为操作上全局天使般的选择。提取的程序的正确性证明通过中间域理论指称语义。我们证明了我们的系统的有用性，通过提取一个并发程序，将无限的格雷码到有符号的数字表示。我们的系统的一个值得注意的特点是，限制和并发性的证明规则涉及到经典的排中律的变体，如果没有Amb，这些变体在计算上是不可解释的。
2022-01-30 cs.LO
Abstract Diagnosis for Timed Concurrent Constraint programs
时间并发约束语言（Timed Concurrent Constraint Language，简称tccp）是一种基于简单但功能强大的并发约束范式Saraswat的并发逻辑语言。在这种范例中，存储作为值的概念被存储作为约束的概念所取代，这引入了与存储作为值的概念的一些差异。其他并发方法。在本文中，我们提供了一个通用的框架调试tccp程序。为此，我们首先提出了一个新的紧凑的，自底向上的语义的语言，非常适合于调试和验证的目的，在反应式系统的上下文中。我们还提供了一个抽象的语义，使我们能够有效地实现基于抽象解释的调试算法。给定一个tccp程序和一个行为规范，我们的调试方法自动检测程序是否满足规范。这与其他半自动调试方法不同，避免了提前提供症状的需要。我们通过介绍两个说明性的例子来展示我们的方法的有效性。我们选择一个特定的抽象域，并展示我们如何可以检测到一个程序是错误的。
2011-09-07 cs.LO cs.PL
Partial Orders for Efficient BMC of Concurrent Software
并发程序中存在的大量交织是导致并发软件自动分析困难的根本原因。人们普遍认为，记忆力差会使这个问题更加困难。我们解决这两个问题的建模程序的执行与偏序，而不是交错语义（SC）。基于这些思想，我们实现了一个软件分析工具。它可以扩展到足够大的程序，以实现对各种型号（包括SC、Intel x86和IBM Power）上的非平凡并发系统代码的首次形式化验证。
2013-01-08 cs.LO cs.PL
Relaxed Operational Semantics of Concurrent Programming Languages
我们提出了一种新颖的，可操作的框架，正式描述的语义并发程序运行在一个宽松的内存模型的上下文中。我们的框架具有一个“临时存储”的内存操作发出的线程记录，在程序顺序。然后，内存模型指定允许全局执行此序列中的挂起操作的条件，可能是无序的。内存模型还涉及“写粒度”，这说明了线程可能读取尚未全局可见的写操作的架构。我们的正式模型是由一个软件模拟器支持，使我们能够在我们的语义运行石蕊测试。
2012-08-14 cs.LO cs.PL
Effect-Dependent Transformations for Concurrent Programs
我们描述了一个指称语义的抽象效果系统的高阶，共享变量并发程序设计语言。我们证明了一些一般的基于效果的程序等价物的合理性，包括并行化方程，该方程指定了用并行组合物替换顺序组合物的充分条件。效果注释是相对于由合约指定的抽象位置而不是物理足迹，这使我们特别能够显示涉及细粒度并发数据结构（例如Michael-Scott队列）的某些转换的可靠性，这些转换允许并发访问可变数据结构的不同部分。我们的语义是基于改进的痕迹为基础的语义的一阶程序，由于布鲁克斯。通过从具体位置移动到抽象位置，并添加类型细化来捕获表达式及其并发环境的可能副作用，我们能够验证许多在未细化模型中不存在的等价性。类型的含义是使用基于游戏的逻辑关系在轨迹集上表达的。两个程序$e_1$和$e_2$是逻辑相关的，如果一个程序能够解决一个两人游戏：对于任何轨迹，结果值$v_1$在$e_1$（挑战）的语义中，玩家提出，对手可以提出一个（响应）等价的轨迹，在$e_2$的语义中，具有逻辑相关的结果值$v_2$。
2015-10-08 cs.LO cs.PL
Barriers in Concurrent Separation Logic: Now With Tool Support!
我们开发并证明了一个合理的并发分离逻辑的Pthreads风格的障碍。尽管Pthreads屏障在系统中被广泛使用，并且分离逻辑被广泛用于验证，但是还没有任何努力将两者结合起来。与锁和临界区不同，Pthreads屏障允许在多个线程之间同时进行资源重新分配，并且本质上是有状态的，导致逻辑设计及其可靠性证明的显着复杂性。我们展示了我们的逻辑可以应用到一个特定的示例程序中的模块化的方式。我们的校样在Coq进行机器检查。我们展示了一个程序验证工具集，自动应用逻辑规则，并履行相关的证明义务。
2012-04-19 cs.LO
Inferring Fences in a Concurrent Program Using SC proof of Correctness
大多数并发程序的证明系统假设底层的内存模型是顺序一致的（SC），这一假设不适用于现代多核处理器。出于性能原因，这些处理器实现了宽松的内存模型。作为这种放松的结果，一个程序，在SC内存模型上被证明是正确的，可能会错误地执行。为了保证其在松弛条件下的正确性，在代码中插入了栅栏指令。在本文中，我们表明，SC证明的算法的正确性，在[Sou84]的证明系统中进行，确定每个线程的指令排序足够的SC证明。此外，为了在底层松弛存储器模型上正确地执行该算法，通过插入栅栏指令仅尊重这些排序就足够了。
2013-04-10 cs.DC cs.LO
Towards linking correctness conditions for concurrent objects and contextual trace refinement
并发对象的正确性条件描述了抽象顺序对象的原子性如何被分解。许多不同的并发对象和证明方法已经发展。然而，关于正确性的论证是针对孤立的对象进行的。这与现实世界的实践形成对比，在现实世界中，并发对象通常被实现为程序设计语言库的一部分（例如，java.util.concurrent），并在客户机程序内被实例化。一个自然的问题是：并发对象的正确性条件如何确保使用并发对象的客户端程序的正确性？本文介绍了围绕这个问题的主要问题，并提供了一些答案，通过链接不同的正确性条件与跟踪细化的形式。
2016-06-07 cs.DC cs.LO
Slicing Concurrent Constraint Programs
并发约束编程（CCP）是一个声明式的并发模型，其中代理通过告诉和询问共享存储中的约束（信息片段）进行交互。以前的一些作品已经开发了（近似）CCP语言的声明式调试器。然而，调试并发程序的任务仍然很困难。在本文中，我们定义了一个动态切片CCP，我们表明它是一个有用的伴侣工具，现有的调试技术。我们的技术首先考虑一个部分计算（跟踪），显示存在的错误。通常，这种跟踪中的信息量是压倒性的，用户很容易迷失方向，因为她不能专注于bug的来源。我们的切片器允许标记计算状态的一部分，并帮助用户消除大部分冗余信息，以突出错误。我们表明，这种技术可以定制CCP的定时变量。我们还开发了一个原型实现免费提供实验。
2017-02-10 cs.LO cs.PL
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
除了前置条件和后置条件，最近的并行分离逻辑中的程序规范采用了一种资源的代数结构-状态转换系统的一种形式-来描述必须保留的基于状态的程序不变量，并记录允许的程序状态原子变化。在本文中，我们引入了一个新的概念，资源态射，即资源上的结构保持功能，并展示了如何有效地将其集成到分离逻辑，使用相关的概念态射特定的模拟。我们将态射和模拟应用于在一种资源下验证的程序，以使它们在另一种资源下运行，从而促进证明重用。
2019-10-15 cs.DC cs.LO cs.PL
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
我们提出了TaDA现场，一个并发分离逻辑的推理组合终止阻塞细粒度并发程序。关键的挑战是如何处理抽象的原子阻塞：也就是说，抽象的原子操作具有阻塞行为，这些阻塞行为来自于例如细粒度自旋锁中的忙等待模式。我们的基本创新是抽象规范的设计，捕捉这种阻塞行为作为对环境的活跃假设。我们设计了一个逻辑，可以原因的客户端使用这些操作的终止，而不会打破他们的抽象边界，和操作的实现相对于他们的抽象规范的正确性。我们引入了一个新的语义模型，使用分层的主观义务来表达活性不变量，和一个证明系统，这是健全的模型。我们的规范和推理的微妙之处说明了使用几个案例研究。
2021-11-30 cs.LO cs.PL
Efficient Verification of Concurrent Programs Over TSO Memory Model
我们解决的问题，多线程程序运行在总存储顺序（TSO）内存模型的有效验证。它已被证明，即使有限的数据域程序，控制状态可达下TSO的复杂性是非原始递归。在本文中，我们首先提出了一种有界缓冲区验证方法，其中缓冲区的大小上的界限放置，验证是递增地进行，通过增加的缓冲区的大小与验证过程的每次迭代，直到达到所述的界限。对于有限数据域上的程序，我们还证明了存在一个缓冲区的界限K，如果该程序是安全的，那么它也是安全的无界缓冲区。我们已经实现了这种技术在一个工具ProofTraPar。我们的结果对memorax [2]，一个国家的最先进的声音和完整的验证TSO记忆模型，一直令人鼓舞。
2016-06-17 cs.LO cs.PL
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
本文提出概率并发结果逻辑（pcOL），用于描述并发和概率程序中变量的联合分布，并通过案例分析推导精确信息，证明无界循环的几乎确定终止。
2025-11-25 cs.LO cs.PL
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Aarhus University（奥胡斯大学）；New York University（纽约大学）；Amazon Web Services（亚马逊云科技）
本文提出Foxtrot，首个用于证明高阶并发概率程序上下文细化的高阶分离逻辑，结合了并发推理原理与概率推理原理，展示了其在对抗性von Neumann硬币和Sodium加密库中的应用。
2026-04-27 cs.LO cs.PL
Compositional Non-Interference for Fine-Grained Concurrent Programs
非干扰性是一种程序属性，可确保不存在信息泄漏。在程序设计语言的上下文中，有两种常见的方法来建立非干扰：类型系统和程序逻辑。类型系统提供了强大的自动化（通过类型检查），但它们在它们支持的程序类型方面有固有的限制。程序逻辑支持具有挑战性的程序，但它们通常需要大量的人工帮助，并且不能处理模块或更高阶的程序。为了连接这两种方法，我们提出了SeLoC-一种非干扰的分离逻辑，在此基础上，我们使用逻辑关系技术建立了一个类型系统。通过在分离逻辑之上构建类型系统，我们可以组合地验证由类型化和非类型化部分组成的程序。前一部分通过型式检验进行验证，后一部分通过人工校对进行验证。SeLoC的核心技术贡献是最弱前提条件的关系形式，可以使用分离逻辑资源跟踪信息流。SeLoC是完全机器检查的，并且构建在Iris框架之上，用于Coq中的并发分离逻辑。与Iris的集成为细粒度并发提供了无缝支持，这是之前的类型系统和程序逻辑无法实现的无干扰性。
2020-03-06 cs.LO cs.PL
Concurrent Separation Logic Meets Template Games
并发理论和程序设计语言语义学的一个古老梦想是揭示基本的同步机制，这些机制调节的情况与高阶程序的游戏语义和具有共享内存和锁的并发程序的霍尔逻辑一样不同。在本文中，我们建立了一个深刻的和意想不到的连接最近的两条工作线并发分离逻辑（CSL）和差分线性逻辑（DiLL）的模板游戏语义。由于这种联系，我们重新制定了纯粹的概念风格的模板游戏为迪尔的异步和交互式的解释CSL设计的梅利斯和Stefanesco。我们相信，分析揭示了一些重要的秘密解剖CSL，更具体地说，微妙的相互作用，分类性质，顺序组成，并行产品，错误和锁之间。
2020-05-09 cs.LO cs.PL
A Spin-based model checking for the simple concurrent program on a preemptive RTOS
我们通过eChronos将现有的RTOS内核抢占式调度模型从机器辅助证明修改为基于Spin的模型检查器。我们构建的模型可以自动验证，而不是用手工证明。此外，我们还研究了一个类似Linux的实时内核--Piko/RT的设计和ARMv7-M体系结构的规范来重建模型，并在内核开发阶段使用LTL来描述一个简单的并发程序--消费者/生产者问题。我们证明了在抢占式调度和ARMv7-M机制下，程序不会出现竞争条件、饥饿和死锁。
2018-08-07 cs.FL cs.LO cs.OS
Compositional Verification in Concurrent Separation Logic with Permissions Regions
本文提出带权限区域的 CSL-Perm 组合式验证系统，通过可推断框架规则残余堆的蕴涵过程实现线程与函数调用推理，并经 CoSl 工具验证其优势。
2025-10-06 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
Quantum Temporal Logic
本文介绍了一种量子并发程序模型，它可用于反应式量子系统的行为建模和量子编译器的设计。我们研究量子时序逻辑，QTL，量子并发系统的规范，建议事件的时间依赖性。QTL将子空间上的投影作为原子命题，这是Birkhoff和von Neumann的经典量子逻辑论文中建立的。对于确定性泛函量子程序，我们证明了一个量子Böhm-Jacobini定理，该定理指出任何这样的程序都等价于一个Q-While程序。研究了一般量子并发程序中QTL基本公式的可判定性。
2019-08-19 cs.LO quant-ph
Non-Sequential Theory of Distributed Systems
这些课堂讲稿涵盖了并发和分布式系统的建模和验证的基本自动机理论概念和逻辑形式。这些概念中的许多自然地扩展了经典的自动机和逻辑，这些概念为建模顺序系统提供了一个框架。另一方面，分布式系统结合了几个（有限或递归）过程，因此将被建模为（分别为有限或下推）自动机的集合。分布式系统的一个关键参数是进程之间允许的交互类型。在这堂课中，我们将重点讨论消息传递范式。通常，分布式系统中的通信在事件之间创建复杂的依赖关系，当使用顺序的操作语义时，这些依赖关系被隐藏。这里采取的方法是基于忠实地保留并发事件的依赖关系。也就是说，系统的执行被建模为偏序或图，而不是事件序列。
2021-10-17 cs.FL cs.LO
Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs
该研究使用Isabelle/HOL验证了一个单遍编译器能够保持混合敏感并发程序的非干扰性，通过引入分解原则简化安全精化证明，并在真实用例上自动保留安全属性。
2022-02-28 cs.CR cs.LO cs.PL
