Formal Verification of Chase-Lev Deque in Concurrent Separation Logic
本论文利用并发分离逻辑并在 Coq proof assistant 中对 Chase-Lev deque 进行了形式化验证，采用无界现实实现与 linearizability 强规范，满足最小可信计算基等三大标准，并扩展支持安全内存回收与松弛内存模型基础。
2023-05-20 cs.LO cs.PL
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
我们报告的中间结果，我们的研究推理活性属性，除了深正确性的一个命令，并发程序设计语言与高阶存储。目前，我们集中在一个特定的活性属性，即终止。通过保证终止性，我们可以将部分正确性的陈述加强为完全正确性。这是通过将终止性转换为安全属性的经典方法来实现的。特别是，我们扩展的程序设计语言考虑与调用权限，这已被证明，使模块化的推理终止。添加原子块是为了增加我们基于调用权限的方法的表现力。我们的工作建立在Iris --一个基础的、机器检查的、高阶并发分离逻辑框架--之上，而不修改它。有了这些补充，我们就能够模块化地推理并发但非阻塞算法的终止。我们对正在考虑的程序设计语言的添加保留了Iris对帮助和预言进行推理的能力。作为一个例子，我们将当前的系统应用于现有的无锁并发堆栈的案例研究，并在Iris中得到了证明。最后，我们概述了扩展阻塞并发方法的后续步骤。
2022-12-28 cs.LO cs.PL
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
基于状态机的符号在组件系统的描述中无处不在，特别是在机器人领域。为了确保这些系统的安全性和可预测性，形式化验证技术是重要的，如果它们是自动化和可扩展的，则可以具有成本效益。在本文中，我们提出了一个验证方法的图形状态机语言，利用定理证明和指称语义的基础上统一编程理论（UTP）。我们提供了必要的理论来支撑状态机（包括迭代过程的归纳定理），机械化状态和转换的动作语言，并使用这些来形式化语义。然后，我们描述的验证方法，它支持无限状态系统，并使用一个完全自动化的死锁自由检查。这项工作已经在我们的证明工具Isabelle/UTP中实现了机械化，因此也说明了使用UTP来构建实用的验证工具。
2018-08-24 cs.LO
Compositional Reasoning for Shared-variable Concurrent Programs
并发系统的可扩展和自动化形式化验证一直是一个迫切的需求。在本文中，我们提出了一个验证框架，以支持自动组合推理的并发程序共享变量。我们的框架模型并发程序作为简洁的自动机，并支持多个重要属性的验证。简洁自动机的安全性验证和仿真是并行组合的，简洁自动机的安全性在精化过程中保持不变。我们以自动化的方式从无限状态并发程序中生成简洁的自动机。此外，我们提出了第一个自动化的方法来检查可靠保证无限状态并发程序之间的模拟。我们已经将我们的算法原型化，并将我们的工具应用于多个改进的验证。
2018-03-26 cs.FL cs.LO cs.SE
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
本研究提出一种嵌入简单类型高阶逻辑的并发命令式程序建模、验证与转换框架，可支持对交错计算命令式程序模型性质的可靠结构化推理，并通过Peterson互斥算法案例验证了其适用性。
2024-07-14 cs.LO
Multi-player Equilibria Verification for Concurrent Stochastic Games
并发随机博弈（Concurrent Stochastic Games，CSG）是一种理想的概率系统建模方法，其特点是多个参与者或组件具有不同的目标，同时做出合理的决策。示例包括通信或安全协议和多机器人导航。存在用于CSG的验证方法，但仅限于代理或玩家被分组为两个联盟的场景，其中同一联盟中的那些共享相同的目标。在本文中，我们提出了多联盟的验证技术的CSG。我们使用子博弈完美的社会福利（或社会成本）的最优纳什均衡，这是战略，没有任何联盟单方面改变其战略在任何游戏状态，并在总的组合目标最大化（或最小化）。我们提出了一个扩展的时序逻辑rPATL（概率交替时间时序逻辑与奖励），指定任何数量的不同联盟的基于均衡的属性，和相应的模型检验算法的一个变体停止游戏。我们实现我们的技术在PRISM游戏工具，并将其应用到几个案例研究，包括秘密共享协议和公益游戏。
2020-07-24 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
Bilateral Proofs of Safety and Progress Properties of Concurrent Programs
本文提出了并发程序的可组合规格说明的一种理论，它允许：（1）对给定规格说明的程序代码进行验证;（2）组合组件的规格说明以产生程序的规格说明。该规范包括在程序执行结束时（如果执行终止）保持的终端属性和在整个执行过程中保持的永久属性。我们设计（1）证明技术的验证，和（2）组合规则，以获得规格的程序，从它的组件。我们利用组件的终端属性导出永久的性质的程序，反之亦然。因此，这种证明策略被称为双边的。该理论的组成方面是很重要的，在组装程序的组件，其中一些源代码可能是不可用的，因为越来越多的情况下，跨供应商的程序集成。
2017-04-05 cs.LO cs.PL
On the Expressivity of Typed Concurrent Calculi
本论文全面探究支撑类型化编程语言的形式化计算模型，聚焦函数式与并发程序演算，指出其为程序语义评估及相关分析、验证技术开发提供严谨框架，为含附录的完整版论文。
2024-08-15 cs.LO cs.PL
Automatic Verification of Concurrent Stochastic Systems
随机游戏的自动验证技术允许对系统进行正式推理，这些系统具有不确定或概率设置中理性代理之间的竞争或协作行为。现有的工具和技术集中于回合制游戏，其中游戏的每个状态由单个玩家控制，以及零和属性，其中两个玩家或联盟具有直接相反的目标。在本文中，我们提出了并发随机游戏（CSG）的自动验证技术，它提供了一个更自然的并发决策和交互模型。我们还考虑（社会福利）纳什均衡，正式确定的情况下，两个球员或联盟有不同的目标可以合作，以优化他们的联合表现。我们提出了一个扩展的时间逻辑rPATL在这种情况下指定的定量属性，并提出相应的算法验证和策略合成的变体停止游戏。对于有限时域的性质，计算是精确的，而对于无限时域，它是近似使用值迭代。对于零和性质，它需要通过线性规划来求解矩阵博弈，对于基于均衡的性质，我们通过SMT编码的标记多面体方法来找到双矩阵博弈的社会福利或社会成本纳什均衡。我们在PRISM游戏中实现了这种方法，这需要扩展工具的建模语言用于CSG，并将其应用于包括机器人技术，计算机安全和计算机网络在内的领域的案例研究，明确展示了CSG和基于平衡的属性的好处。
2020-08-29 cs.LO
A Note on Runtime Verification of Concurrent Systems
本文提出基于Mazurkiewicz迹的三值LTrL运行时验证方法，通过迹一致Büchi自动机构造监控器，使同一迹的所有线性化得到一致的验证结论。
2025-07-07 cs.FL cs.LO cs.SE
Partial Orders for Efficient BMC of Concurrent Software
并发程序中存在的大量交织是导致并发软件自动分析困难的根本原因。人们普遍认为，记忆力差会使这个问题更加困难。我们解决这两个问题的建模程序的执行与偏序，而不是交错语义（SC）。基于这些思想，我们实现了一个软件分析工具。它可以扩展到足够大的程序，以实现对各种型号（包括SC、Intel x86和IBM Power）上的非平凡并发系统代码的首次形式化验证。
2013-01-08 cs.LO cs.PL
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
设计可扩展的并发对象，它可以有效地用于多核处理器，往往需要放弃标准的规范技术，如线性化，有利于更宽松的一致性要求。然而，各种各样的替代正确性条件使得在特定情况下难以选择使用哪一个，并且在使用其行为通过不同标准指定的对象时难以组合它们。缺乏句法验证方法的大多数这些标准构成了挑战，在他们的系统采用和应用。在本文中，我们认为使用霍尔风格的程序逻辑作为一种替代和统一的方法规范和组合形式化验证的并发对象及其客户端程序的安全属性。通过一系列的案例研究，我们展示了如何现有的程序逻辑的并发性可以采用现成的捕捉重要的状态和历史不变，允许一个明确量化的环境线程的干扰，并提供直观和富有表现力的霍尔式规范的几个非线性并发对象，以前只指定通过专用的正确性标准。我们通过验证一些并发客户端的情况下，利用以前指定的并发对象，捕捉并发意识的线性化，静态和定量静态一致性等正确性条件的本质，说明我们的规范的充分性。本文中描述的所有示例都在Coq中进行了机械验证。
2016-07-21 cs.LO cs.PL
Model Checking Data Flows in Concurrent Network Updates (Full Version)
我们提出了一个模型检验的方法来验证数据流的正确性，在网络配置的并发更新。该验证问题对于软件定义网络（SDN）非常重要，其中错误可能导致分组丢失、黑洞和安全违规。我们的方法是基于规范的时间属性的个人数据流，如要求流是免费的周期。我们检查这些属性是否同时满足所有活动的数据流，而网络配置更新。为了表示并发网络控制器的行为和由此产生的配置的演变，我们引入了一个扩展的Petri网的过境关系，其特征在于由Petri网的每个转变所引起的数据流。对于安全的Petri网与过境，我们减少了时间流属性的验证电路模型检验问题，可以解决有效的验证技术，如IC3，插值，有界模型检验。我们报告令人鼓舞的实验与原型实现的基础上的硬件模型检查ABC。
2019-11-14 cs.LO
Verifying Temporal Properties of Reactive Systems by Transformation
我们展示了如何程序转换技术可以用于验证反应系统的安全性和活性特性。特别是，我们展示了如何程序转换技术蒸馏可以用来转换反应系统指定的功能语言成一个简化的形式，随后可以分析，以验证系统的时间属性。示例系统的目的是模型互斥分析使用这些技术的安全性（互斥）和活性（非饥饿），与错误，它们包含被正确识别。
2015-12-12 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
Abstract Diagnosis for Timed Concurrent Constraint programs
时间并发约束语言（Timed Concurrent Constraint Language，简称tccp）是一种基于简单但功能强大的并发约束范式Saraswat的并发逻辑语言。在这种范例中，存储作为值的概念被存储作为约束的概念所取代，这引入了与存储作为值的概念的一些差异。其他并发方法。在本文中，我们提供了一个通用的框架调试tccp程序。为此，我们首先提出了一个新的紧凑的，自底向上的语义的语言，非常适合于调试和验证的目的，在反应式系统的上下文中。我们还提供了一个抽象的语义，使我们能够有效地实现基于抽象解释的调试算法。给定一个tccp程序和一个行为规范，我们的调试方法自动检测程序是否满足规范。这与其他半自动调试方法不同，避免了提前提供症状的需要。我们通过介绍两个说明性的例子来展示我们的方法的有效性。我们选择一个特定的抽象域，并展示我们如何可以检测到一个程序是错误的。
2011-09-07 cs.LO cs.PL
Towards Concurrent Quantitative Separation Logic
本文提出并发定量分离逻辑，将定量分离逻辑与并发分离逻辑结合，用于验证并发、指针和随机化程序实现后置条件的概率下界。
2024-09-30 cs.LO cs.PL
Shared Memory Concurrent System Verification using Kronecker Algebra
多线程软件的验证仍然是一个挑战。这主要是因为线程交织的数量在线程数量中呈指数级增长。用矩阵演算研究线交织是这一研究领域的一种新方法。我们的程序的稀疏矩阵表示使用Kronecker代数的惰性实现进行操作。一个目标是生成一个称为并发程序图（CPG）的数据结构，它描述了所有可能的交织，并在保持完整性的同时结合了同步。我们证明了CPG在一般情况下可以表示为稀疏邻接矩阵。因此，矩阵中的条目数与其行数成线性关系。因此，有效的算法可以应用于CPG。此外，由于同步，实际上只需要结果矩阵的很小一部分，而其余部分在自动机方面是不可达到的。由于矩阵运算的延迟实现，无法到达的部分永远不会计算。这大大加快了处理速度，表明这种方法非常有前途。可以在CPG上执行包括数据流分析在内的各种应用。此外，矩阵的结构可以用来证明任意数量的线程的底层程序的属性。例如，死锁自由证明了一大类程序。
2011-09-26 cs.LO
Robust Verification of Concurrent Stochastic Games
Department of Computer Science, University of Oxford, Oxford OX1 2JD, UK（计算机科学系，牛津大学，牛津 OX1 2JD，英国）
本文提出鲁棒并发随机游戏模型及验证框架，用于处理多智能体系统中转移概率的不确定性问题。
2026-01-21 cs.AI cs.GT cs.LO
Barriers in Concurrent Separation Logic: Now With Tool Support!
我们开发并证明了一个合理的并发分离逻辑的Pthreads风格的障碍。尽管Pthreads屏障在系统中被广泛使用，并且分离逻辑被广泛用于验证，但是还没有任何努力将两者结合起来。与锁和临界区不同，Pthreads屏障允许在多个线程之间同时进行资源重新分配，并且本质上是有状态的，导致逻辑设计及其可靠性证明的显着复杂性。我们展示了我们的逻辑可以应用到一个特定的示例程序中的模块化的方式。我们的校样在Coq进行机器检查。我们展示了一个程序验证工具集，自动应用逻辑规则，并履行相关的证明义务。
2012-04-19 cs.LO
Towards modular verification of pathways: fairness and assumptions
模块化验证是一种用于解决并发交互系统等复杂系统的性能验证中经常遇到的状态爆炸问题的技术。模块化方法是基于这样的观察，即感兴趣的属性通常只涉及系统的一小部分。因此，可以构建简化的模型，其近似于整个系统的行为，从而允许更有效的验证。生物化学途径可以被看作是复杂的并发交互系统。因此，验证它们的属性通常在计算上非常昂贵，并且可以利用模块化方法。在本文中，我们报告的生化途径的模块化验证框架的发展的初步结果。我们认为生物化学途径是竞争分子资源的并行反应系统。模块化验证技术可以基于仅包含涉及感兴趣的分子资源的反应的简化模型。对于一个适当的描述系统的行为，我们认为，它是必不可少的考虑一个合适的公平性的概念，这是一个完善的概念，并发理论，但在该领域的新途径建模。我们提出了一个建模方法，包括公平性，我们确定的假设下，验证属性可以在一个模块化的方式。我们证明了这种方法的正确性，并证明它的模型上的EGF受体诱导的MAP激酶级联Schoeberl等。
2012-11-17 cs.LO
Unifying Theories of Reactive Design Contracts
契约式设计是基于模型设计的一种重要技术，其中组合系统由指定每个组件的行为假设和保证的契约集合指定。在本文中，我们描述了一个统一的理论反应式设计合同的反应式系统的建模和验证提供了基础。我们提供了一种语言的表达和组成的合同，是由一个丰富的计算理论支持。与文献中的其他语义模型相比，我们的合同理论允许我们指定状态变量的演变和允许与环境的相互作用。此外，我们的互动模型是抽象的，并支持，例如，离散时间，连续时间，和混合计算模型。基于统一编程理论（UTP），我们的理论可以与进一步的计算理论相结合，以支持多范式语言的语义。通过我们的证明框架Isabelle/UTP提供了实际的推理支持，包括一个证明策略，该策略将关于反应式程序的猜想减少到三个谓词，象征性地描述其假设并保证中间和最终观察结果。这使我们能够验证具有大或无限状态空间的程序。我们的工作推进了最先进的反应式语言的语义，他们的合同规范的描述，和组合验证。
2019-09-09 cs.LO
A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification
本文讨论的问题，指定，模拟和验证反应系统重写逻辑。它提出了一个可执行的语义概率，时间和空间并发约束编程-这里称为随机和空间并发约束系统（SSCC）-在重写逻辑语义框架。该方法是基于一个增强和广义模型的并发约束规划（CCP）的计算层次空间可以分配给属于代理。可执行语义忠实地表示和操作捕捉高度并发的性质，不确定的行为，空间和认知特征的反应系统与信息流。在SSCC中，定时属性（由随机持续时间表示）可以与进程相关联，并且还支持排他性和独立的概率选择。利用Maude系统中的SMT求解技术，实现了SSCC的底层约束系统，包括整数和实数上的无量词公式。这导致了一个完全可执行的实时符号规范，可用于定量分析的统计模型检验的形式。SSCC的主要特点和能力说明了整个文件的例子。这一贡献是一个更大的研究工作的一部分，旨在提供正式的分析技术和工具，数学上建立在CCP的方法，研究界。
2022-11-03 cs.LO
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
Formalization of Automated Trading Systems in a Concurrent Linear Framework
我们提出了一个声明性和模块化规范的自动交易系统（ATS）的并发线性框架CLF。我们在Celf中实现了它，这是一个CLF类型检查器，也支持执行CLF规范。我们概述了验证的两个代表性的交易系统使用生成语法，CLF规范的推理方法。
2019-04-15 cs.LO
On Reducing Linearizability to State Reachability
原子对象（如并发堆栈和队列）的有效实现特别容易受到编程错误的影响，并且需要自动验证。不幸的是，他们的正确性标准-相对于给定的ADT规格的线性化-很难验证。即使在通常的时间安全属性（如控制状态可达性）是可判定的实现类上，线性化也是不可判定的。在这项工作中，我们证明了验证线性化某些固定ADT规格是可减少控制状态的可达性，尽管更难任意ADT。我们实现了几个最流行的原子对象的这种减少。这种减少产生的第一个可判定性结果的验证，而不限制并发线程的数量。此外，它使现有的安全验证工具的线性化验证的应用。
2015-05-25 cs.LO
Automated Verification of Quantum Protocols by Equivalence Checking
本文介绍了一种用于各种量子信息处理协议形式化验证的技术和工具。该工具采用稳定器形式化，能够表示并发量子协议，比量子电路更具有表达能力。我们还报告了使用我们的量子等价性（QEC）来分析一系列量子信息处理协议的实验结果。
2013-12-20 cs.LO
Correlated Equilibria and Fairness in Concurrent Stochastic Games
博弈论技术和均衡分析促进了竞争系统的设计和验证。虽然均衡计算的算法复杂性已被广泛研究，但博弈论方法的实际实现和应用是最近才出现的。工具，如PRISM游戏支持自动验证和合成的零和和（ε-最优子博弈完美）社会福利纳什均衡性能并发随机游戏。然而，这些方法变得效率低下的代理人的数量增长，也可能产生的均衡，产生显着的变化，个别代理人的结果。相反，我们考虑相关的均衡，其中玩家可以通过公共信号进行协调，并引入一个替代的社会公平的最优性标准，它可以应用于纳什均衡和相关均衡。我们发现，相关的均衡更容易计算，更公平，也可以改善联合结果。我们实现了范式游戏和更复杂的情况下，多玩家并发随机游戏的时间逻辑规范的算法。
2022-02-01 cs.GT cs.LO
A beginner guide to Iris, Coq and separation logic
本指南面向初学者，介绍使用 Iris 和 Coq 进行形式化验证，重点讲解示例、策略、分离逻辑，并全面覆盖相关工具，以帮助读者安全验证并发算法。
2025-01-23 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
CCS-Based Dynamic Logics for Communicating Concurrent Programs
这项工作提出了三个日益表现力的动态逻辑，其中的程序是CCS进程（sCCS-PDL，CCS-PDL和XCCS-PDL）。他们的目标是推理使用CCS描述的并发程序和系统的属性。为了实现这一点，CCS的操作符和结构被添加到基本模态逻辑中，以创建适合于描述和验证通信，并发和非确定性程序和系统的属性的动态逻辑，类似于PDL用于顺序情况。我们提供完整的公理化的三个逻辑。与Peleg的带通道的并发PDL不同，我们的逻辑具有简单的Kripke语义、完备的公理化和有限模型性质。
2009-04-01 cs.LO
Automated Synthesis of Distributed Controllers
LaBRI, University of Bordeaux（波尔多大学）
本文探讨了在Mazurkiewicz轨迹设定下分布式综合的概念及其在去中心化运行时监控中的应用，针对并发程序验证与分析的挑战提出新的方法。
2015-06-08 cs.FL cs.LO cs.SY
Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
University of Twente（特温特大学）；TU Delft（代尔夫特理工大学）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出在VerCors中编码弱内存并发的方案，通过扩展原子操作支持并引入协议自动机概念，实现基于许可的分离逻辑，用于验证弱内存并发程序的正确性。
2026-04-22 cs.LO
Sheaves and geometric logic and applications to the modular verification of complex systems
在本文中，我们表明，并发系统的状态，转移和行为往往可以建模为一个合适的拓扑空间上的层。在这种情况下，几何逻辑可以用来描述当互连系统时，在全局级别上保留哪些局部属性（即单个系统的属性）。主要应用领域是复杂系统的模块化验证。我们说明的想法，通过一个例子，涉及一个家庭的相互作用的控制器的火车上的铁路轨道。
2008-10-16 cs.LO
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
我们提供了简单的等式原则，推导出可靠保证风格的推理规则和细化法律的基础上幂等半环。我们将代数层与基于语言和执行轨迹的程序的具体模型联系起来。我们已经实现了伊莎贝尔/HOL的方法作为一个轻量级的并发验证工具，支持推理的控制和数据流的并发程序在不同层次的抽象共享变量。这在两个简单的验证示例中进行了说明。
2013-12-04 cs.DC cs.LO
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。
2017-10-30 cs.DC cs.FL cs.LO
Automated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic
在这项工作中，我们提供了算法解决方案的五个基本问题的验证，合成和校正的并发系统，可以建模有界p/t-网。我们表示并发通过偏序，并假设行为规范通过一元二阶逻辑。c-偏序是Hasse图可以被c路覆盖的偏序。对于有限的变迁集T，设P（c，T，n）表示所有T-标号的c-偏序满足n的集合。若N=（P，T）是p/t-网，则P（N，c）表示N的所有c-偏序游程的集合。一个（b，r）-有界p/t-网是一个b-有界p/t-网，其中每个位置最多重复出现r次。我们解决了以下问题：1.验证：给定一个MSO公式n和一个有界p/t网N，确定P（N，c）是否\subseteq P（c，T，n），P（c，T，n）是否\subseteq P（N，c），或P（N，c）\cap P（c，T，n）是否= \emptyset。2.根据MSO质量标准合成：给定一个MSO公式n，合成一个满足P（c，T，n）\subseteq P（N，c）的语义极小（b，r）-有界p/t-网N. 3.语义最安全子系统：给定一个定义安全偏序集的MSO公式，和一个可能包含不安全行为的b-有界p/t-net N，合成出行为介于P（N，c）\cap P（c，T，N）和P（N，c）之间的最安全的（b，r）-有界p/t-net N'. 4.行为修复：给定两个MSO公式\cap P（c，T，）和一个b-有界p/t-网N，合成一个语义极小（b，r）-有界p/t…
2014-02-11 cs.DC cs.DS cs.LO
Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model
为了利用多核和分布式平台的强大功能，并使软件工程师更容易开发并发软件，已经提出了不同的面向对象的并发模型，如SCOOP。尽管分析SCOOP程序的实际重要性，目前还没有通用的验证方法，直接对程序代码进行操作，而无需额外的注释。其中一个原因是SCOOP的大量部分冲突的语义形式化（无论是在理论上还是在实现上）。在这里，我们提出了一个简单的图形转换系统（GTS）为SCOOP的运行时语义，掌握所有已知的语义语言的最常见的功能。这个运行时模型是在最先进的GTS工具GROOVE中实现的，它使我们能够模拟，分析和验证SCOOP程序的一个子集的死锁和其他行为属性。除了提出第一种方法来验证SCOOP程序的自动翻译GTS，我们还强调我们的经验，应用GTS（特别是GROOVE）指定语义的形式，运行时模型，这应该是转移到GTS模型的其他并发语言和库。
2015-04-10 cs.DC cs.LO cs.PL
Verifying that a compiler preserves concurrent value-dependent information-flow security
通常通过对源代码进行推理来证明程序不会泄漏敏感数据。但是这样做在推理和现实之间留下了一个缺口，只能通过解释编译器的行为来填补。当程序强制执行值相关的信息流安全属性（其中位置的分类可以根据其他位置中的值而变化）时，此任务是复杂的，并且当程序利用共享变量并发时进一步复杂化。先前的工作已经正式定义了并发感知的概念，以保持值依赖的安全属性的细化。然而，这个概念要比标准的精化定义复杂得多，标准的精化定义通常应用于编译器对语义保持的验证。到目前为止，还不清楚它是否可以应用于一个现实的编译器，因为不存在一般的分解原则，将其分为更小，更熟悉，证明义务。在这项工作中，我们提供了这样一个分解原则，我们表明，几乎可以一半的复杂性证明安全的细化。此外，我们证明了它的适用性，安全编译，通过证明在伊莎贝尔/HOL的保存值依赖的安全性的概念证明编译器从一个命令式的，而语言到一个通用的RISC风格的汇编语言，为程序与共享内存并发介导的锁定原语。最后，我们执行我们的编译器在伊莎贝尔的跨域桌面合成器的语言模型，展示了我们的知识，第一次使用的编译器验证结果进行信息流的安全属性到一个非平凡的并发程序的汇编级模型。
2019-07-01 cs.CR cs.LO cs.PL
Coalgebraic Tools for Bisimilarity and Decorated Trace Semantics
并发反应式系统的建模、规范和语义研究已经成为一个有趣的研究课题。本论文的目的是利用（共）代数框架的优势，在建模反应系统和推理的几种类型的相关语义，在一个统一的方式。特别是，我们感兴趣的处理概念的行为等价/前序范围从双相似性的系统，可以表示为非确定性的coalgebras，装饰跟踪语义标记的过渡系统和概率系统，并测试语义标记的过渡系统的内部行为。此外，我们的目标是推导出一套相应的验证算法，适合在自动化工具中实现。
2015-02-10 cs.FL cs.LO
Safety verification of asynchronous pushdown systems with shaped stacks
在本文中，我们研究了通过无界和无序消息缓冲区通信的并发下推系统的程序点可达性问题。我们的目标是放宽通常的限制，即消息只能在堆栈为空时由下推进程检索。我们使用部分交换上下文无关文法的概念来描述一类新的异步通信的下推系统与一个温和的形状约束栈的程序点的可覆盖性问题仍然是可判定的。符合形状约束的堆栈可以达到任意高度;此外，进程可以执行任何通信动作（无论是进程创建，消息发送还是检索），无论其堆栈是否为空。这个类扩展了以前在异步程序的上下文中研究的计算模型，并使一大类消息传递程序的安全性验证成为可能。
2014-01-24 cs.FL cs.LO cs.PL
CTL* Verification and Synthesis using Existential Horn Clauses
Technion - Israel Institute of Technology（以色列理工学院）
本文提出基于存在性Horn子句（EHCs）的自动验证与合成方法，用于无限状态反应程序对CTL*规格的验证，展示了其在复杂系统中的应用。
2024-08-21 cs.LO
Parametric Verification: An Introduction
本文对并发系统的参数验证作了一个简短的介绍。它起源于在托鲁塞（2016）和萨拉戈萨（2017）的Petri网会议上举行的两次为期一天的教程。本文不仅介绍了视频版本中处理的基本形式概念，而且还提供了广泛的文献，为读者提供进一步的参考，涵盖该领域。我们首先介绍了一般参数验证背后的动机，然后重点介绍了不同的模型和方法，用于验证几种类型的系统。它们包括参数时间自动机，用于实时系统建模，其中时间约束不一定是先验已知的。类似地，参数区间马尔可夫链允许对事件发生概率是具有参数边界的区间的系统进行建模。参数Petri网允许系统的紧凑表示，并处理不同类型的参数。最后，动作合成的目的是在并发系统中启用或禁用动作，以保证其某些属性。在本教程的实践课上使用了一些实施这些方法的工具。相应的实践可以在网上免费获得。
2019-07-01 cs.LO cs.SE
Reactive Synthesis Without Regret
无限持续时间的两个玩家零和游戏及其定量版本用于验证控制器（夏娃）和它的环境（亚当）之间的相互作用模型。通常要解决的问题是，夏娃是否有一个策略（和可计算性），可以最大化她对亚当的任何策略的回报。在这项工作中，我们感兴趣的策略，夏娃，最小化她的遗憾，即策略，最小化之间的差异，她的实际收益和她可能已经实现，如果她事先知道亚当的策略。我们给出算法来计算夏娃的策略，以确保最小的遗憾对对手的选择的战略是（一）不受限制，（二）限于位置的战略，或（三）限于字的战略。我们还建立了后者的版本和其他问题之间的关系，在文献中研究。
2021-10-28 cs.FL cs.GT cs.LO
Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest
通信是使多智能体系统能够合作的关键部分。这意味着将形式化方法应用于多智能体系统内的通信协议，可以为其可靠性提供有用的信心。在本文中，我们描述了形式化验证的一个复杂的通信协议，协调代理合并他们的环境的地图。LFC团队在2019年的多智能体编程竞赛（MAPC）中使用了该协议。我们的协议规范是写在通信顺序进程（CSP），这是一个非常适合的方法来指定智能体通信协议，由于其重点是并发通信系统。我们使用已知正确行为的场景来验证规范的行为，并验证最终所有映射都已合并。
2021-06-22 cs.LO cs.MA
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
本文提出将 LLM 代码生成与基于形式化方法的反应式程序综合结合，通过分工处理复杂逻辑，并构建基准验证其可解决以往 LLM 难以完成的代码生成问题。
2024-09-18 cs.LG cs.LO cs.SE
