Modular Verification of Concurrent Programs via Sequential Model Checking
这项工作利用了过多的工作验证顺序程序的目的，验证并发程序。我们减少了一个并发程序的验证一系列的顺序程序的验证任务。我们的方法是模块化的，在这个意义上，每个顺序的验证任务大致对应于一个线程的验证，与一些额外的信息，它在其中运行的环境。根据需要，在算法运行期间收集关于环境的信息。虽然我们的方法是通用的，它专门针对线程层次结构的并发程序。这个想法是利用层次结构，以最大限度地减少需要在线程之间传输的信息量。为此，我们验证的线程之一，认为“主”，作为一个顺序程序。它的验证过程向它的“环境”（可能包含多个线程）发起查询。如果环境由单个线程组成，则通过顺序验证来回答这些查询，否则，通过在环境上应用相同的分层算法来回答这些查询。我们的技术是全自动的，并允许我们使用任何现成的顺序模型检查器。我们实现了我们的技术在一个工具，称为CoMuS和评估它对建立并发验证工具。我们的实验表明，它的工作特别好的层次结构的程序。
2021-06-01 cs.PL
Modular GPU Programming with Typed Perspectives
Massachusetts Institute of Technology（麻省理工学院）；University of Pennsylvania（宾夕法尼亚大学）
针对GPU编程中线程级控制与集体操作协同的冲突导致模块化代码易出错的问题，提出带类型化视角的GPU语言Prism，可在不损失性能的前提下保障模块化编程的安全性。
2025-11-14 cs.DC cs.PL
Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
National University of Singapore（新加坡国立大学）
本文提出通过摘要驱动的抽象解释方法，结合锁集摘要和线程ID推理，显著提升数据竞争检测的准确性。
2025-11-25 cs.PL cs.SE
CPC: programming with a massive number of lightweight threads
线程是编写并发程序的一种方便和模块化的抽象，但通常相当昂贵。线程的标准替代方案，事件循环编程，允许更轻的并发单元，但导致代码难以编写，甚至更难理解。Continuation Passing C（CPC）是一个翻译器，可根据程序员的选择，将以线程风格编写的程序转换为使用事件和本机系统线程编写的程序。我们与两名本科生一起，通过编写Hekate自学了如何在CPC中编程，Hekate是一个大规模并发网络服务器，旨在有效地处理成千上万的同时连接的对等体。在本文中，我们描述了一些编程习惯用法，我们在写Hekate时学到的;虽然其中一些习惯用法是特定于CPC的，但许多应该适用于其他具有足够便宜的线程的编程系统。
2011-02-04 cs.PL
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker
由于增加每个CPU插槽的处理单元数量的强烈趋势，因此多线程程序变得越来越重要。我们介绍了一种新的可配置的程序分析验证多线程程序的线程数有限。我们提出了一个简单而有效的实现现有的程序验证框架CPAchecker的组成部分。虽然CPAchecker已经在一个大型的基准集的顺序验证任务的竞争力，我们的扩展增强了框架的整体适用性。我们处理多线程的实现与数据流分析的抽象域是正交的，因此，可以与CPAcchecker中的几种现有分析相结合，如值分析，区间分析和BDD分析。新的分析是模块化的，可以用来，例如，验证可达性属性以及检测程序中的死锁。本文包括一些优化步骤的效益评估（例如，改变可达性算法的迭代顺序或应用偏序约简）以及与用于验证多线程程序的其它现有技术工具的比较。
2016-12-15 cs.LO cs.PL cs.SE
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
近年来，随着操作语义和相关逻辑的发展，C11程序的演绎验证技术有了很大的进步。然而，这些语义和逻辑是在受限的环境中开发的，以避免稀薄空气读取问题。在本文中，我们提出了一个操作语义，利用线程内的偏序（称为语义依赖）诱导最近开发的指称事件结构为基础的语义。我们证明了我们的操作语义是健全的和完整的指称语义。我们提出了一个相关的逻辑，概括了最近Owicki-Gries框架RC 11（修复C11），并证明了使用这种逻辑的几个例子证明。
2021-08-03 cs.LO cs.PL
Compiler Testing With Relaxed Memory Models
针对现有并发编译器测试技术无法兼顾边界内漏洞覆盖与大规模程序可扩展性的问题，提出工业级测试工具Téléchat，通过对比源与架构内存模型下的程序行为发现漏洞，性能优于现有技术且已部署应用。
2024-01-29 cs.AR cs.PL cs.SE
RacerF: Lightweight Static Data Race Detection for C Code
本文提出RacerF，一种基于Frama-C平台的轻量级静态分析工具，通过上下近似方法实现线程模块化数据竞争检测，在保证高精度的同时提升检测速度。
2025-06-18 cs.PL cs.SE
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs
我们提出了一个静态分析的抽象解释检查运行时间错误的并行和多线程的C程序。在我们的工作Astrée，我们专注于嵌入式关键程序没有递归，也没有动态内存分配，但扩展到一个静态的线程集的分析，通过共享内存和显式地使用一组有限的互斥锁隐式通信，并根据实时的【形】调度策略和固定的优先级调度。我们的方法是线程模块化的。它是基于一个稍微修改的非平行分析，当分析一个线程，应用和丰富的一组抽象的线程冲突。然后迭代器依次重新分析每个线程，直到冲突稳定下来。我们证明了我们的方法的可靠性顺序一致性语义，但也相对于一个合理的弱一致的内存语义。我们还展示了如何考虑互斥和线程优先级，通过分区的抽象调度状态。我们展示了使用原型Thésée分析工业程序的初步实验结果，并展示了我们方法的可扩展性。
2012-03-22 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
Verifying C11 Programs Operationally
本文提出了一个操作语义的释放-获取片段的C11内存模型与宽松的访问。我们表明，语义是健全的和完整的公理模型。语义依赖于每个线程的可观察性概念，这使得人们可以按照程序顺序对弱内存C11程序进行推理。在此之上，我们开发了一个证明演算为基础的不变量推理，我们用它来验证释放获取版本的彼得森的互斥算法。
2018-11-22 cs.DC cs.PL
Operational Aspects of C/C++ Concurrency
在这项工作中，我们提出了一个家庭的操作语义，逐渐接近现实的程序行为的C/C++11内存模型。我们框架中的每个语义都是通过阐述和组合两个简单的成分构建的：视图和操作缓冲区。视图允许我们表达线程交互的空间方面，即，线程可以读取哪些值，而操作缓冲器使得能够利用时间执行方面进行操纵，即，确定某些操作的结果可以被并发运行的线程观察到的顺序。从一个简单的抽象状态机开始，通过一系列的抽象状态的逐步细化，我们捕获这样的语言方面和同步原语的释放/获取原子，顺序一致和非原子内存访问，还提供了一个语义放松原子，同时避免了稀薄空气的问题。据我们所知，这是C11的第一个正式的和可执行的操作语义，能够表达标准的所有基本并发方面。我们说明了我们的方法，通过一些特征的例子，有关观察到的行为，从文献中的标准石蕊测试程序。我们提供了一个可执行的PLT Redex中的语义实现，以及一些实现的石蕊测试和示例，并展示了我们的原型上的一个大型案例研究：随机测试和调试一个现实的读取-复制-更新数据结构。
2016-07-09 cs.PL
Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning (Extended Version)
University of California, Santa Cruz（加利福尼亚大学圣克鲁兹分校）；Williams College（威廉姆斯学院）
研究多线程软件正确性推理中RG逻辑函数规范难复用问题，提出移动逻辑，通过原子函数概念扩展RG逻辑，避免稳定化要求，实用验证器已证其优势，移动逻辑为该领域未来工作奠定基础。
2026-07-28 cs.PL
An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model
KU Leuven, Department of Computer Science, DistriNet Research Group（荷语鲁汶大学计算机科学与DistriNet研究组）
提出一种模块化验证方法，通过交错操作语义连接 (Y)C20 公理模型与 Iris 等并发程序逻辑，以验证 Rust ARC 核心且不依赖程序序与 reads-from 并集无环假设。
2025-09-26 cs.PL
2LS for Program Analysis
2LS（“tools”）是一个基于CPROVER框架的C程序验证工具。它允许验证用户指定的断言，内存安全属性（例如缓冲区溢出），数值溢出，除以零，内存泄漏和终止属性。分析是通过将验证任务转换为二阶逻辑公式，包括位向量、数组和浮点算术理论来执行的。该公式是解决了一个模块化的组合算法，涉及展开和基于模板的不变合成的帮助下，增量SAT解决。2LS的优点包括其非常快速的增量有界模型检验算法和其灵活的框架，用于试验新的分析和抽象思想的不变推理。缺点是它缺乏对某些程序特性的支持（例如多线程）。
2023-02-05 cs.LO cs.PL cs.SE
Pointer Race Freedom
我们提出了一个新的概念指针竞争的并发程序操纵一个共享堆。指针竞争是对已释放的内存地址的访问，无论单元是否已重新分配，都不受访问者的控制。我们建立了两个结果。(1)在指针竞争自由的假设下，验证一个程序在显式存储管理下运行，就像它在垃圾回收下运行一样是合理的。(2)甚至指针竞争自由本身的要求也可以在垃圾收集语义下得到验证。然后，我们证明了类似的定理，一个更强的概念，指针种族需要处理性能关键的代码，故意使用活泼的比较，甚至活泼的指针引用。作为一个实际的贡献，我们应用我们的结果来优化显式存储管理下的线程模块化分析。我们的实验证实了高达两个数量级的加速。
2015-11-11 cs.PL
Verifying C11-Style Weak Memory Libraries
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成，该操作语义使客户端程序执行它使用的库中的抽象方法调用的验证成为可能。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2020-12-28 cs.LO cs.PL
Dynamic Verification with Observational Equivalence of C/C++ Concurrency
松弛内存模型（rmm）语义下的程序执行更难分析; rmm语义导致程序事件的乱序执行，导致状态空间爆炸。动态偏序约简（DPOR）是一种解决这种状态空间爆炸的强大技术，已被用于验证RMM下的程序，如TSO，PSO和POWER。这种DPOR技术的核心是跟踪等价的概念，它是基于程序事件之间的独立关系计算的。我们提出了一个粗糙的概念，称为观测等价（OE）的RMM感知跟踪等价。如果每个读事件在两个行为中读取相同的值，则两个程序行为在观察上是等效的。我们提出了一个概念的观测独立性（OI），并提供了一个算法的建设，以计算迹等价（模OI）有效。我们还证明了DPOR与OE线程C/C++程序的有效性，首先提供了一个精心制作的happensbefore（HB）的关系捕捉C/C++并发语义。我们实现了一个运行时模型检查称为Drista的技术。我们的实验表明，（i）与现有的nonOE技术相比，我们实现了显着节省的跟踪下探索OE的数量，（ii）我们的治疗C/C++并发性比现有的国家的最先进的技术更广泛。
2022-07-30 cs.DC cs.PL
Verifying C11-Style Weak Memory Libraries via Refinement
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的，负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成在一起，该操作语义可以验证客户端程序从他们使用的库中执行抽象方法调用。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2021-08-16 cs.LO cs.PL
