An Interactive Proof of Termination for a Concurrent $λ$-calculus with References and Explicit Substitutions

一种高阶并发终止保持精化逻辑

A Higher-Order Logic for Concurrent Termination-Preserving Refinement

高阶并发语言的更精确的正确性证明是困难的：它们涉及到在并发的高级源语言和使用低级共享内存原语的实现之间建立一个保持终止的精化。然而，现有的逻辑证明并发加细要么忽略属性，如终止，或只处理一阶状态。在本文中，我们解决这些限制，扩展虹膜，最近的高阶并发分离逻辑，支持终止保留的细化推理。为了证明这些扩展的功能，我们证明了一个高阶，会话类型的语言的有效实现的正确性。据我们所知，这是第一个能够为这种语言提供编译器正确性证明的程序逻辑。我们的扩展和我们的编译器正确性证明的合理性已经在Coq中机械化。

Modular termination verification with a higher-order concurrent separation logic (Intermediate report)

We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enabl…

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients which use …

并发量子程序的可达性和可终止性分析

Reachability and Termination Analysis of Concurrent Quantum Programs

我们介绍了并发量子程序的马尔可夫链模型。该模型是Hart，Sharir和Pnueli概率并发程序的量子推广。通过分析并发量子程序的可达空间、一致重复可达空间和可终止性的数学结构，给出了它们的一些特征。在此基础上，给出了计算可达空间、一致重复可达空间和判定终止性的算法。

参数化概率并发系统的公平终止（技术报告）

Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)

我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。

解决并发安全性和可达性游戏的终止标准

Termination Criteria for Solving Concurrent Safety and Reachability Games

我们考虑图上的并发博弈。在游戏的每一轮，每个玩家同时独立地选择一步棋，这些棋步共同决定了向后继状态的过渡。两个基本目标是永远停留在一组给定状态的安全性目标，以及它的对偶，到达一组给定状态的可达性目标。本文提出了一种计算并发安全对策值的策略改进算法，即局中人1实现安全目标的最大概率。该算法产生一个序列的玩家-1的策略，以确保获胜的概率，单调收敛到安全游戏的值。我们的结果是显着的，因为策略改进算法提供了，第一次，一种方法来近似值的并发安全游戏从下面。由于值迭代算法，或可达性游戏的策略改进算法，可以用来近似相同的值从上面，这两种算法的组合产生一种方法，用于计算收敛序列的上限和下限的并发可达性和安全游戏的值。以前的方法只能从一个方向近似这些游戏的值，并且由于没有已知的收敛速度，它们没有提供解决这些游戏的实用方法。