paperbot · PL 论文追踪

全部论文 待读 收藏

标签：并发、并行与内存模型（共 651 篇，按优先级展示前 200）

P1 Sound Static Data Race Verification for C: Is the Race Lost?
C 语言的健全静态数据竞争验证：这场竞争输了吗？
通过真实程序基准与代码惯用法微基准，揭示健全静态数据竞争验证工具的能力、局限与不健全性。
TOPLAS 47(3)2025匹配度 6/10引用 3程序分析与抽象解释程序验证并发、并行与内存模型
P1 Deterministic parallel fixpoint computation
确定性并行不动点计算
提出弱偏序 WPO 与确定性并行不动点算法，并通过 Pikos 在抽象解释中获得显著加速。
POPL 4(POPL)2019匹配度 5/10引用 9程序分析与抽象解释并发、并行与内存模型
P1 Freeing hybrid distributed AI training configuration
解放混合分布式 AI 训练配置
提出并行语义分析方法，自动选择混合并行策略，相比数据并行取得 260% 加速。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 5/10引用 3机器学习与程序语言并发、并行与内存模型
P1 CXLMC: Model Checking CXL Shared Memory Programs
CXLMC：CXL 共享内存程序的模型检测
提出 CXLMC，对 x86-CXL 共享内存程序的崩溃执行进行模型检测，在 8 个应用中发现 24 个缺陷。
ASPLOS Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22026匹配度 5/10引用 2程序验证并发、并行与内存模型
P1 Concurrency verification with maximal path causality
基于最大路径因果性的并发验证
提出最大路径因果性模型，把到达同一路径的调度与输入组合归为等价类，统一探索并发程序调度与输入空间。
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 5/10引用 2程序验证并发、并行与内存模型
P1 Tail Modulo Async-Await
异步等待下的尾模优化
将尾调用优化扩展到异步调用，提出 TMA 变换，避免多余任务，并可与 TMC 结合实现并行且空间优化的递归函数。
ICFP 10(ICFP)2026匹配度 5/10编译与代码生成并发、并行与内存模型
P1 Soundness of Predictive Concurrency Analyses
预测性并发分析的健全性
统一并推广预测性并发分析的健全性定义，提出三步证明模板，并证明六个已有分析（含首个弱内存分析）健全。
OOPSLA 9(OOPSLA1)2025匹配度 5/10并发、并行与内存模型程序分析与抽象解释
P2 Fast, sound, and effectively complete dynamic race prediction
快速、可靠且有效完备的动态数据竞争预测
提出多项式时间且无假阳性的动态数据竞争预测算法 M²，对两进程完备并可动态判定完备性。
POPL 4(POPL)2019匹配度 4/10引用 46并发、并行与内存模型程序验证
P2 Concurrent incorrectness separation logic
并发不正确性分离逻辑
将不正确性分离逻辑扩展到并发程序，提供参数化框架检测竞态、死锁和内存安全错误并保证真阳性。
POPL 6(POPL)2022匹配度 4/10引用 24程序验证并发、并行与内存模型
P2 PerSeVerE: persistency semantics for verification under ext4
PerSeVerE：ext4 下用于验证的持久性语义
形式化 ext4 与 C/C++ 弱内存的持久性语义，提出模型检测验证方法并发现编辑器缺陷。
POPL 5(POPL)2021匹配度 4/10引用 21形式语义程序验证并发、并行与内存模型
P2 Automating CUDA Synchronization via Program Transformation
通过程序变换自动实现 CUDA 同步
提出 AuCS，首个在 LLVM 级对 CUDA 内核自动插入同步屏障的通用框架，可处理数据竞争、屏障分歧与冗余屏障。
ASE 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE)2019匹配度 4/10引用 20编译与代码生成并发、并行与内存模型
P2 An Empirical Study on Concurrency Bugs in Interrupt-Driven Embedded Software
中断驱动嵌入式软件中并发缺陷的实证研究
首次大规模实证分析工业中断驱动嵌入式软件中的132个真实并发缺陷，总结其根因、影响、修复与表现形式。
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 4/10引用 17并发、并行与内存模型测试、调试与修复
P2 Bounded Verification of Multi-threaded Programs via Lazy Sequentialization
基于惰性顺序化的多线程程序有界验证
提出惰性顺序化，将有界多线程 C 程序转为串行程序，复用 BMC 高效验证并发。
TOPLAS 44(1)2021匹配度 4/10引用 16程序验证并发、并行与内存模型
P2 Game of Threads
线程的游戏
论文关注异步机器学习训练中多线程竞争式更新模型所引发的问题。
ASPLOS Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems2020匹配度 4/10引用 15机器学习与程序语言并发、并行与内存模型
P2 Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation
使用局部化抽象解释检测 Go 程序中的阻塞错误
提出局部化抽象解释方法，用于检测 Go 程序中由基于 channel 的并发导致的阻塞错误。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 4/10引用 14程序分析与抽象解释并发、并行与内存模型
P2 Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
结果逻辑中的概率并发推理：独立性、条件化与不变式
提出 pcOL，首个能表达概率并发程序完整结果分布的程序逻辑，并支持几乎必然终止等推理。
POPL 10(POPL)2026匹配度 4/10引用 14程序验证并发、并行与内存模型
P2 Data Race Freedom à la Mode
模式化数据竞争自由
扩展 OCaml 类型系统，以 mode 保证多线程数据竞争自由并兼容顺序代码。
POPL 9(POPL)2025匹配度 4/10引用 11类型系统并发、并行与内存模型定理证明与证明工程
P2 Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models
面向 SC、TSO 和 PSO 内存模型的模序一致性理论可满足性
提出适用于 SC、TSO 和 PSO 内存模型的序一致性理论及 SMT 求解器 Zord，显著提升并发程序验证性能。
TOPLAS 45(1)2023匹配度 4/10引用 10并发、并行与内存模型程序验证
P2 A Compositional Deadlock Detector for Android Java
面向 Android Java 的组合式死锁检测器
为超大规模 Android Java 应用提出组合式静态死锁检测，基于临界对将问题判定为 NP 并部署于 Infer。
ASE 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)2021匹配度 4/10引用 9程序分析与抽象解释并发、并行与内存模型
P2 Towards Unified Analysis of GPU Consistency
迈向 GPU 一致性模型的统一分析
将 PTX 与 Vulkan 一致性模型集成到 Dartagnan，实现首个可分析真实 GPU 代码的多模型验证工具，并发现原模型两处缺陷。
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 42024匹配度 4/10引用 8并发、并行与内存模型程序验证
P2 Tolerate Control-Flow Changes for Sound Data Race Prediction
容忍控制流变化以实现可靠的数据竞争预测
提出不动点事件与偏序模型，可可靠推断带控制流变化的见证轨迹，从而检测更多数据竞争。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 4/10引用 5并发、并行与内存模型程序分析与抽象解释
P2 vCXLGen: Automated Synthesis and Verification of CXL Bridges for Heterogeneous Architectures
vCXLGen：面向异构架构的 CXL 桥自动合成与验证
提出 CXL 桥抽象并实现 vCXLGen，可从机器可读的一致性协议规范自动合成并组合验证异构 CXL 桥。
ASPLOS Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22026匹配度 4/10引用 5程序合成程序验证并发、并行与内存模型
P2 SpecChecker-ISA: a data sharing analyzer for interrupt-driven embedded software
SpecChecker-ISA：面向中断驱动嵌入式软件的数据共享分析器
提出基于抽象解释数值不变式的数据共享分析器，可靠且精确地识别中断驱动程序中的共享数据访问。
ISSTA Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis2022匹配度 4/10引用 3程序分析与抽象解释并发、并行与内存模型
P2 Robustness Verification for Checking Crash Consistency of Non-volatile Memory
非易失性内存崩溃一致性检查的鲁棒性验证
提出全自动鲁棒性验证工具 PMVerify，用符号编码、SMT 与 DPLL(T) 检测 NVM 程序的崩溃一致性缺陷。
ASPLOS Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 12025匹配度 4/10引用 2程序验证并发、并行与内存模型
P2 Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
通过稀疏傅里叶学习实现 Linux 内核中精确的数据竞争预测
将执行轨迹可行性建模为稀疏布尔函数并用稀疏傅里叶学习求解，提升 Linux 内核数据竞争预测精度与发现数量。
OOPSLA 8(OOPSLA1)2024匹配度 4/10引用 2机器学习与程序语言并发、并行与内存模型
P2 A Probabilistic Choreography Language for PRISM
面向 PRISM 的概率编排语言
提出一种概率编排语言，定义概率语义并编码到 PRISM，支持并发概率系统的全局建模与模型检测。
LMCS vol.Volume 22, Issue 42026匹配度 4/10并发、并行与内存模型量子与概率编程程序验证
P2 GoPV: A Static Analyzer for Finding Blocking Concurrency Bugs Due to Misuse of Shared-Memory Synchronization in Go
GoPV：一种用于发现 Go 中因共享内存同步误用导致的阻塞并发缺陷的静态分析器
GoPV 静态分析器基于调用图与（后）支配者分析，检测 Go 程序中共享内存同步误用导致的阻塞并发缺陷。
ISSTA Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis2025匹配度 4/10程序分析与抽象解释并发、并行与内存模型
P2 Static Analysis of Memory Models for SMT Encodings
面向 SMT 编码的内存模型静态分析
通过内存模型静态分析计算关系边界，并优化 SMT 编码，加速有界模型检测。
OOPSLA 7(OOPSLA2)2023匹配度 4/10程序分析与抽象解释程序验证并发、并行与内存模型
P2 A static verification framework for message passing in Go using behavioural types
基于行为类型的 Go 消息传递静态验证框架
提出基于行为类型的静态验证框架，用于检查 Go 通道消息传递程序的并发正确性。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10引用 72类型系统并发、并行与内存模型
P2 TriCheck
TriCheck
提出全栈内存一致性模型验证工具流 TriCheck，并揭示 RISC-V 与 C11 间的规范漏洞与低效。
ASPLOS Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems2017匹配度 3/10引用 67并发、并行与内存模型程序验证
P2 Automated Synthesis of Comprehensive Memory Model Litmus Test Suites
自动合成全面的内存模型 litmus 测试套件
提出自动合成全面内存模型 litmus 测试套件的方法，以覆盖弱内存模型的隐蔽边界情况。
ASPLOS Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems2017匹配度 3/10引用 55并发、并行与内存模型测试、调试与修复
P2 Exceptional asynchronous session types: session types without tiers
异常异步会话类型：无需层级（tiers）的会话类型
首次将异步会话类型与异常处理集成到函数式语言，给出核心演算与 Links 实现。
POPL 3(POPL)2019匹配度 3/10引用 52并发、并行与内存模型类型系统函数式编程
P2 Truly stateless, optimal dynamic partial order reduction
真正无状态的最优动态偏序归约
提出 TruSt 算法，使并发程序动态偏序归约同时做到每等价类仅探索一个交错且内存消耗为线性。
POPL 6(POPL)2022匹配度 3/10引用 45程序验证并发、并行与内存模型
P2 VSync: push-button verification and optimization for synchronization primitives on weak memory models
VSync：弱内存模型上同步原语的一键式验证与优化
提出 VSync 框架，自动检测弱内存模型同步原语中缺失与过度约束的内存屏障，并验证其安全与活性。
ASPLOS Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems2021匹配度 3/10引用 40并发、并行与内存模型程序验证
P2 On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
弱内存一致性下的库正确性：声明式一致性模型中并发库的规约与验证
提出声明式框架，在弱内存一致性下对并发库进行组合式规约与验证。
POPL 3(POPL)2019匹配度 3/10引用 37并发、并行与内存模型程序验证
P2 A separation logic for concurrent randomized programs
并发随机化程序的分离逻辑
提出支持概率推理的并发分离逻辑 Polaris，并机器化验证随机化并发计数器与跳表。
POPL 3(POPL)2019匹配度 3/10引用 37程序验证并发、并行与内存模型定理证明与证明工程
P2 Parallel complexity analysis with temporal session types
基于时间会话类型的并行复杂度分析
提出时间会话类型，将线性逻辑会话类型扩展以局部、组合地分析并发消息传递程序的参数化并行复杂度。
ICFP 2(ICFP)2018匹配度 3/10引用 37类型系统并发、并行与内存模型
P2 UFO
UFO：精确预测并发释放后使用漏洞
提出 UFO，通过扩展最大线程因果模型与约束求解，从单次轨迹精确预测并发 UAF，无假阳性且可扩展。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10引用 35并发、并行与内存模型程序分析与抽象解释
P2 Optimal prediction of synchronization-preserving races
同步保持型竞态的最优预测
提出同步保持型竞态，并给出可靠完备、时空近最优的预测算法，证明其恰为竞态预测可处理边界。
POPL 5(POPL)2021匹配度 3/10引用 35并发、并行与内存模型程序分析与抽象解释
P2 Compositional bisimulation metric reasoning with Probabilistic Process Calculi
基于概率进程演算的组合性双模拟度量推理
提出用一致连续性刻画概率进程演算中双模拟度量语义的组合推理，并支持递归过程与度量式假设保证性能验证。
LMCS vol.Volume 12, Issue 42017匹配度 3/10引用 35形式语义并发、并行与内存模型
P2 Automatically detecting and fixing concurrency bugs in go software systems
自动检测并修复 Go 软件系统中的并发缺陷
提出 GCatch 与 GFix，自动检测并修复 Go 中因 channel 误用导致的阻塞型并发缺陷。
ASPLOS Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems2021匹配度 3/10引用 31程序分析与抽象解释测试、调试与修复并发、并行与内存模型
P2 HMC
HMC
提出 HMC，面向硬件内存模型的无状态模型检测，支持 load buffering 并兼顾效率与可扩展性。
ASPLOS Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems2020匹配度 3/10引用 29程序验证并发、并行与内存模型
P2 Simulee
Simulee
提出首个轻量级 CUDA 同步缺陷检测框架 Simulee，通过解释 LLVM 字节码收集访存信息来自动检测同步缺陷。
ICSE Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering2020匹配度 3/10引用 27并发、并行与内存模型测试、调试与修复
P2 A true positives theorem for a static race detector
静态竞态检测器的真阳性定理
为 RacerD 静态竞态检测器证明真阳性定理，并给出与原版对比的实现评估。
POPL 3(POPL)2019匹配度 3/10引用 26程序分析与抽象解释并发、并行与内存模型
P2 Mechanized relational verification of concurrent programs with continuations
带续延的并发程序的机械化关系验证
首个全形式化工具，机械化关系验证带 call/cc 与 throw 的并发高阶命令式程序。
ICFP 3(ICFP)2019匹配度 3/10引用 24程序验证定理证明与证明工程并发、并行与内存模型
P2 Automated Verification of Go Programs via Bounded Model Checking
基于有界模型检测的 Go 程序自动验证
提出基于有界模型检测的 Go 并发程序静态检查器，可处理大型代码库与静态未知参数，性能优于现有工具。
ASE 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)2021匹配度 3/10引用 22程序验证并发、并行与内存模型
P2 Static Detection of Event-based Races in Android Apps
Android 应用中基于事件的竞态的静态检测
提出静态工具 SIERRA，通过统一动作序、上下文抽象与按需路径敏感分析精确检测 Android 事件驱动竞态。
ASPLOS Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems2018匹配度 3/10引用 21程序分析与抽象解释并发、并行与内存模型
P2 Multiparty GV: functional multiparty session types with certified deadlock freedom
Multiparty GV：具有经认证无死锁性的函数式多参与方会话类型
提出函数式多参与方会话类型语言MPGV，支持一等端点并保持无死锁性，结果已在Coq中机器验证。
ICFP 6(ICFP)2022匹配度 3/10引用 21类型系统并发、并行与内存模型
P2 Weak-consistency specification via visibility relaxation
通过可见性松弛的弱一致性规范
提出可见性松弛注释语言，为多一致性级别操作提供弱一致性规范并支持有效验证。
POPL 3(POPL)2019匹配度 3/10引用 20并发、并行与内存模型程序验证
P2 Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
常数树宽组件并发系统中的代数路径性质算法
为常数树宽组件的并发系统提出代数路径性质查询算法，实现预处理与查询时间权衡并改进最坏情况复杂度。
TOPLAS 40(3)2018匹配度 3/10引用 20程序分析与抽象解释并发、并行与内存模型
P2 Games for Bisimulations and Abstraction
双模拟与抽象的博弈
用 Spoiler-Duplicator 博弈统一刻画分支、延迟、η 与弱双模拟，并辅助诊断实现与规约的不一致。
LMCS vol.Volume 13, Issue 42017匹配度 3/10引用 20形式语义并发、并行与内存模型
P2 FlakeRepro: automated and efficient reproduction of concurrency-related flaky tests
FlakeRepro：并发相关不稳定测试的自动化高效复现
提出 FlakeRepro，结合静态与动态分析高效复现并发导致的不稳定测试失败，探索数十个交错即可复现相同错误。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 3/10引用 16测试、调试与修复并发、并行与内存模型
P2 Exploiting the laws of order in smart contracts
利用智能合约中的顺序规律
提出 EthRacer，用偏序归约与动态符号执行检测以太坊智能合约的事件排序漏洞。
ISSTA Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis2019匹配度 3/10引用 16程序分析与抽象解释并发、并行与内存模型
P2 Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels
Plume：高效且完备的弱隔离级别黑盒检查
提出首个高效、完备的弱隔离级别黑盒检查器 Plume，可检测数据库隔离缺陷并生成反例。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 16并发、并行与内存模型程序验证
P2 Connectivity graphs: a method for proving deadlock freedom based on separation logic
连接图：一种基于分离逻辑证明无死锁的方法
提出连接图抽象，用分离逻辑证明无死锁与无内存泄漏，并在 Coq 中机械化，首次为高阶二元会话类型语言提供机械化证明。
POPL 6(POPL)2022匹配度 3/10引用 16并发、并行与内存模型程序验证
P2 Reference Capabilities for Flexible Memory Management
用于灵活内存管理的引用能力
提出基于引用能力的属主类型系统，强制 Verona 中区域隔离，支持对象跨区域与线程移动，且数据访问无需原子操作。
OOPSLA 7(OOPSLA2)2023匹配度 3/10引用 15类型系统并发、并行与内存模型
P2 Scheduling constraint based abstraction refinement for weak memory models
面向弱内存模型的基于调度约束的抽象精化
将 SCAR 抽象精化扩展到 TSO/PSO 弱内存模型，显著提升多线程程序验证效率。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 3/10引用 14程序验证并发、并行与内存模型
P2 Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs
GPU 程序中数据竞争的可靠且部分完备静态分析
提出 GPU 数据竞争检测的真阳性定理与近似分析，实现首个可靠且部分完备的检测器 FaialAA。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 14程序分析与抽象解释并发、并行与内存模型
P2 Parameterized verification under TSO is PSPACE-complete
TSO 下的参数化验证是 PSPACE 完全的
证明 TSO 下参数化并发程序可达性问题是 PSPACE 完全，并刻画初始读与原子 RMW 对复杂度的影响。
POPL 4(POPL)2019匹配度 3/10引用 14程序验证并发、并行与内存模型
P2 Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Kater：自动化弱内存模型元理论与一致性检查
将弱内存模型元理论问题归约为正则语言包含，并自动生成一致性检查，集成到 GenMC。
POPL 7(POPL)2023匹配度 3/10引用 13并发、并行与内存模型逻辑与自动机程序验证
P2 Propositions-as-types and shared state
命题即类型与共享状态
将共享可变状态融入会话并发语言的命题即类型线性逻辑解释，并保持安全与活性。
ICFP 5(ICFP)2021匹配度 3/10引用 13类型系统并发、并行与内存模型
P2 Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
无死锁分离逻辑：线性性为依赖高阶消息传递带来进展
提出线性并发分离逻辑 LinearActris，用线性性保证依赖高阶消息传递程序无死锁且无泄漏。
POPL 8(POPL)2024匹配度 3/10引用 12程序验证并发、并行与内存模型
P2 Decoupling lock-free data structures from memory reclamation for static analysis
将无锁数据结构与内存回收解耦以进行静态分析
提出将无锁数据结构验证与内存回收解耦的静态分析方法，实现 Michael&Scott 和 DGLM 队列的全自动线性一致性验证。
POPL 3(POPL)2019匹配度 3/10引用 12程序验证并发、并行与内存模型
P2 Predictive Monitoring against Pattern Regular Languages
面向模式正则语言的预测性运行时监控
提出面向模式正则语言的预测性运行时监控，能在并发执行重排序中暴露高层时序违规，并给出常空间流式线性时间算法。
POPL 8(POPL)2024匹配度 3/10引用 11程序验证并发、并行与内存模型逻辑与自动机
P2 Stratified Commutativity in Verification Algorithms for Concurrent Programs
并发程序验证算法中的分层交换性
将交换性关系作为并发程序验证中的一等对象，提出抽象交换性框架与分层组合证明规则。
POPL 7(POPL)2023匹配度 3/10引用 11程序验证并发、并行与内存模型
P2 Probabilistic Resource-Aware Session Types
概率资源感知会话类型
提出概率会话类型与嵌套多重宇宙语义，实现自动期望资源分析并开发 NomosPro 工具。
POPL 7(POPL)2023匹配度 3/10引用 11类型系统并发、并行与内存模型
P2 CAAT: consistency as a theory
CAAT：一致性作为一种理论
提出一族可刻画多种内存一致性模型的逻辑理论及通用高效求解器，并用于有界模型检测。
OOPSLA 6(OOPSLA2)2022匹配度 3/10引用 11并发、并行与内存模型程序验证
P2 DStream: A Streaming-Based Highly Parallel IFDS Framework
DStream：基于流式处理的高度并行 IFDS 框架
提出流式外存计算与细粒度数据并行的 IFDS 框架 DStream，显著降低内存占用并加速大规模程序分析。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 3/10引用 10程序分析与抽象解释并发、并行与内存模型
P2 Crash-Stop Failures in Asynchronous Multiparty Session Types
异步多方会话类型中的崩溃停止故障
提出带崩溃停止故障的异步多方会话类型理论，借助崩溃处理分支与全局语义，证明良类型进程在崩溃下仍保证无死锁与活性。
LMCS vol.Volume 21, Issue 22025匹配度 3/10引用 10并发、并行与内存模型形式语义
P2 Timed Session Types
时间化会话类型
提出时间化会话类型，给出判定合规性与构造最精确合规对端（及子类型可判定性）的可靠完备技术。
LMCS vol.Volume 13, Issue 42017匹配度 3/10引用 10并发、并行与内存模型类型系统
P2 The Chemical Approach to Typestate-Oriented Programming
Typestate 导向编程的化学方法
提出基于化学隐喻的 typestate 导向编程，以消息分子和化学反应建模并发状态变换，并用行为类型控制对象协议与共享。
TOPLAS 39(3)2017匹配度 3/10引用 10类型系统并发、并行与内存模型
P2 LLM-Based Java Concurrent Program to ArkTS Converter
基于LLM的Java并发程序到ArkTS转换器
用 LLM 思维链分链翻译 Java 并发程序为 ArkTS，并以 ThreadBridge 库在 ArkTS 上模拟 Java 共享内存模型。
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 3/10引用 9机器学习与程序语言并发、并行与内存模型
P2 A programming model for semi-implicit parallelization of static analyses
面向静态分析半隐式并行化的编程模型
提出受响应式编程启发的半隐式并行化编程模型，让分析开发者无需自行处理并发即可并行化静态分析。
ISSTA Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis2020匹配度 3/10引用 9程序分析与抽象解释并发、并行与内存模型
P2 How Hard Is Weak-Memory Testing?
弱内存测试有多难？
证明多种弱内存模型下一致性测试在参数有界时仍 NP 完全，并与 SC、x86-TSO、PSO、Relaxed 形成计算分离。
POPL 8(POPL)2024匹配度 3/10引用 9并发、并行与内存模型逻辑与自动机
P2 Multris: Functional Verification of Multiparty Message Passing in Separation Logic
Multris：分离逻辑中多参与方消息传递的功能正确性验证
提出 Multris 分离逻辑，用多参与方协议一致性验证消息传递与共享内存并发程序的功能正确性。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 9程序验证并发、并行与内存模型
P2 A theory of transaction parallelism in blockchains
区块链中的交易并行理论
提出基于静态分析的区块链交易并行理论，使节点并行执行交易以提升吞吐量。
LMCS vol.Volume 17, Issue 42021匹配度 3/10引用 9程序分析与抽象解释并发、并行与内存模型
P2 AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM
AtoMig：自动将百万行代码从 TSO 迁移到 WMM
提出 AtoMig，自动为百万行级 x86 TSO 代码迁移到 WMM 插入所需同步，避免依赖人工专家。
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22023匹配度 3/10引用 8并发、并行与内存模型编译与代码生成
P2 Commutativity in Automated Verification
自动化验证中的交换性
提出利用迹理论与交换性，将原验证任务替换为更简单的等价程序进行可靠验证。
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 3/10引用 8程序验证并发、并行与内存模型
P2 Datalog-based scalable semantic diffing of concurrent programs
基于 Datalog 的并发程序可扩展语义差分
提出基于 Datalog 的快速近似静态分析，通过识别差异化数据流边来计算并发程序的同步语义差异。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 3/10引用 8程序分析与抽象解释逻辑与约束编程并发、并行与内存模型
P2 Robustness Against Transactional Causal Consistency
针对事务性因果一致性的鲁棒性
研究事务程序对因果一致性的鲁棒性验证，并归约为顺序一致性下的状态可达性。
LMCS vol.Volume 17, Issue 12021匹配度 3/10引用 8并发、并行与内存模型程序验证
P2 CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution Analysis
CSSTs：并发执行分析中用于偏序的动态数据结构
提出 CSSTs 数据结构，以 O(log n) 维护并发执行分析中的偏序，支持插入、删除和查询。
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32024匹配度 3/10引用 7程序分析与抽象解释并发、并行与内存模型
P2 A Relational Separation Logic for Effect Handlers
面向 effect handlers 的关系分离逻辑
提出首个面向 effect handlers 的关系分离逻辑 blaze，支持在含可变状态与并发的程序中证明程序间关系性质。
POPL 10(POPL)2026匹配度 3/10引用 7程序验证并发、并行与内存模型
P2 Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels
面向事务隔离级别正确性检查的动态偏序归约
提出覆盖 Read Committed、因果一致性、快照隔离与可串行化的动态偏序归约模型检测算法，完备、可靠、最优且多项式内存。
PLDI 7(PLDI)2023匹配度 3/10引用 7程序验证并发、并行与内存模型
P2 Modular Termination Verification of Single-Threaded and Multithreaded Programs
单线程与多线程程序的模块化终止性验证
提出一种模块化规约与验证方法，用方法名多重集等层级表达式证明面向对象程序（含堆修改与并发）的终止性与活性。
TOPLAS 40(3)2018匹配度 3/10引用 7程序验证并发、并行与内存模型
P2 Dynamic Deadlock Verification for General Barrier Synchronisation
通用屏障同步的动态死锁验证
提出 Armus：基于 phaser 的事件图模型，为 X10 与 Java 实现可靠完备的动态屏障死锁检测与避免。
TOPLAS 41(1)2018匹配度 3/10引用 7程序验证并发、并行与内存模型
P2 PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency
PipeSynth：面向内存一致性的微架构公理自动合成
提出 PipeSynth，在 RTL 实现完成之前自动合成处理器的微架构内存一致性公理，以支持早期形式验证。
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32023匹配度 3/10引用 4并发、并行与内存模型语言与体系结构
P2 Symbolic execution-driven extraction of the parallel execution plans of Spark applications
符号执行驱动的 Spark 应用并行执行计划抽取
提出符号执行驱动方法，抽取带分支或循环的 Spark 应用可能的多条并行执行计划，替代唯一计划假设。
FSE Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2019匹配度 3/10引用 4程序分析与抽象解释并发、并行与内存模型
P2 ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
ArchSem：可复用的宽松架构严格语义
提出架构通用框架 ArchSem，模块化组合 ISA 与并发模型，并在 Rocq/Isabelle 中实例化 Arm/RISC-V 以支持严格验证。
POPL 10(POPL)2026匹配度 3/10引用 4形式语义并发、并行与内存模型定理证明与证明工程
P2 Validating IoT Devices with Rate-Based Session Types
使用基于速率的会话类型验证 IoT 设备
提出带周期递归的定时进程演算与基于速率的会话类型，保证 IoT 消息传递的速率正确性，并在 Rust 中实现原型。
OOPSLA 7(OOPSLA2)2023匹配度 3/10引用 4并发、并行与内存模型类型系统
P2 Nested Session Types
嵌套会话类型
为会话类型引入 prenex 多态与嵌套递归数据类型，证明类型等价可判定并提出高效可靠算法。
TOPLAS 44(3)2022匹配度 3/10引用 4并发、并行与内存模型类型系统
P2 A predictive analysis for detecting deadlock in MPI programs
一种用于检测 MPI 程序死锁的预测分析
提出单路径 MPI 程序的预测分析，通过依赖图、抽象机与 SMT 求解检测其他可行调度下的死锁。
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 3/10引用 3程序分析与抽象解释并发、并行与内存模型
P2 Work Analysis with Resource-Aware Session Types
资源感知会话类型的工作量分析
提出资源感知会话类型，静态推导消息传递并发进程的最坏情况总工作量。
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 3/10引用 3类型系统并发、并行与内存模型
P2 IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
IsoPredict：用于检测弱隔离数据存储应用中不可串行化行为的动态预测分析
首个面向弱隔离数据存储应用的动态预测分析，通过SMT求解预测可行的不可串行化执行。
PLDI 8(PLDI)2024匹配度 3/10引用 3并发、并行与内存模型程序验证
P2 Lowerbounds for Bisimulation by Partition Refinement
基于划分精化的双模拟判定算法下界
证明了使用划分精化的顺序与并行双模拟判定算法的时间下界，分别为 Ω((m+n) log n) 与 Ω(n)。
LMCS vol.Volume 19, Issue 22023匹配度 3/10引用 3形式语义并发、并行与内存模型
P2 Leaf: Modularity for Temporary Sharing in Separation Logic
Leaf：分离逻辑中临时共享的模块化
提出 Iris 分离逻辑库 Leaf，以 guarding 算子统一临时共享状态，支持模块化并发验证。
OOPSLA 7(OOPSLA2)2023匹配度 3/10引用 3程序验证并发、并行与内存模型
P2 A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
保持 stutter 的偏序归约中不一致标记问题的详细论述
本文指出保持 stutter 的偏序归约早期 stubborn sets 条件存在错误，给出反例并提出更强条件与正确性证明。
LMCS vol.Volume 17, Issue 32021匹配度 3/10引用 3程序验证并发、并行与内存模型
P2 An order-aware dataflow model for parallel Unix pipelines
面向并行 Unix 管道的有序感知数据流模型
提出顺序感知的数据流模型以精确刻画并行 Unix 管道语义，并证明其并行化变换的正确性。
ICFP 5(ICFP)2021匹配度 3/10引用 3形式语义并发、并行与内存模型
P2 SmallRace: Static Race Detection for Dynamic Languages - A Case on Smalltalk
SmallRace：面向动态语言的静态竞态检测——以 Smalltalk 为例
提出 SmallRace，将 Smalltalk 翻译为统一指针类型的 SmallIR，用过程间线程敏感指针分析实现静态竞态检测。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 3/10引用 2程序分析与抽象解释并发、并行与内存模型
P2 A program verification based approach to find data race vulnerabilities in interrupt-driven program
一种基于程序验证的方法：发现中断驱动程序中的数据竞争漏洞
提出基于程序验证的方法检测中断驱动程序中的数据竞争漏洞，旨在消除静态分析中的误报。
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 3/10引用 2程序验证并发、并行与内存模型
P2 On the correctness of GPU programs
论GPU程序的正确性
指出现有CPU测试准则无法直接用于GPU程序，需针对GPU内存与执行模型建立新的测试质量度量与用例生成方法。
ISSTA Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis2019匹配度 3/10引用 2测试、调试与修复并发、并行与内存模型
P2 Sip4J: Statically Inferring Access Permission Contracts for Parallelising Sequential Java Programs
Sip4J：静态推断访问权限契约以并行化顺序 Java 程序
提出 Sip4J，通过跨过程静态分析自动推断 Java 访问权限契约，识别可并发方法以并行化顺序程序。
ASE 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE)2019匹配度 3/10引用 2程序分析与抽象解释并发、并行与内存模型
P2 The Complexity of Testing Message-Passing Concurrency
消息传递并发测试的复杂度
系统刻画通道式消息传递并发一致性测试的复杂度版图，给出近最优算法与实验验证。
POPL 10(POPL)2026匹配度 3/10引用 2并发、并行与内存模型程序验证
P2 DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
DafnyMPI：一个用于验证消息传递并发程序的 Dafny 库
提出 DafnyMPI 库，使 Dafny 能验证 MPI 程序的无死锁、终止与功能等价。
POPL 10(POPL)2026匹配度 3/10引用 2程序验证并发、并行与内存模型
P2 SuperCollider: Scalable and Effective Data Race Detection for CUDA
SuperCollider：面向 CUDA 的可扩展且有效的数据竞争检测
提出 SuperCollider，一种仅跟踪线程级状态、无内存开销且可扩展的 CUDA 数据竞争检测器。
PLDI 10(PLDI)2026匹配度 3/10引用 2并发、并行与内存模型测试、调试与修复
P2 Distributed controller synthesis for deadlock avoidance
死锁避免的分布式控制器合成
提出两种限制使带锁系统的分布式死锁避免控制器合成可判定，并刻画其精确复杂度。
LMCS vol.Volume 21, Issue 32025匹配度 3/10引用 2并发、并行与内存模型逻辑与自动机
P2 Model Checking C/C++ with Mixed-Size Accesses
混合大小访问的 C/C++ 模型检测
提出 Mixer——面向混合大小访问程序的最优 DPOR 算法，并在 GenMC 中实现，首次自动验证此类 C/C++ 并发代码。
POPL 9(POPL)2025匹配度 3/10引用 2程序验证并发、并行与内存模型
P2 Characterizing Implementability of Global Protocols with Infinite States and Data
刻画具有无限状态与数据的全局协议的可实现性
对带无限状态与数据的符号通信协议，给出可实现性的精确语义刻画、检查算法及复杂度结果。
OOPSLA 9(OOPSLA1)2025匹配度 3/10引用 2并发、并行与内存模型程序验证
P2 Opportunistically Parallel Lambda Calculus
机会式并行 Lambda 演算
提出基于 lambda 演算的机会式求值策略，自动并行分派独立外部调用并流式返回结果，并用 Opal 语言验证。
OOPSLA 9(OOPSLA2)2025匹配度 3/10引用 2并发、并行与内存模型语言设计与特性
P2 Efficient Decrease-and-Conquer Linearizability Monitoring
高效的减而治之线性一致性监控
提出减而治之框架，将线性一致性监控归约为识别保线性一致值，并为常见并发数据类型给出多项式乃至近线性时间算法。
OOPSLA 9(OOPSLA2)2025匹配度 3/10引用 2并发、并行与内存模型程序验证
P2 Compositionality and Observational Refinement for Linearizability with Crashes
崩溃下线性一致性的组合性与观测精化
提出带崩溃的并发计算组合模型和 crash-aware linearizability，并给出首个验证崩溃下线性一致性的程序逻辑。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 2并发、并行与内存模型程序验证形式语义
P2 Automated Verification of Parametric Channel-Based Process Communication
参数化基于通道的进程通信的自动验证
提出将 Go 参数化通道通信片段翻译为核心语言并编码为 Dafny 程序，自动验证无部分死锁并推断前置条件。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 2程序验证并发、并行与内存模型
P2 Parallelism in a Region Inference Context
区域推断上下文中的并行性
为基于区域推断的编译器设计 fork-join 并行构造，并给出类型规则、动态语义、类型可靠性及效应推断算法。
PLDI 7(PLDI)2023匹配度 3/10引用 2并发、并行与内存模型运行时与内存管理类型系统
P2 Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility
Armada：具有可靠语义可扩展性的并发代码自动验证
提出 Armada 语言与工具，借助 SMT 自动化和可扩展的可靠推理技术，低代价形式验证高性能并发程序。
TOPLAS 44(2)2022匹配度 3/10引用 2程序验证并发、并行与内存模型
P2 Synthesizing fine-grained synchronization protocols for implicit monitors
为隐式监视器合成细粒度同步协议
提出从隐式监视器合成细粒度显式同步协议的静态分析与 MaxSAT 方法，生成可媲美专家手写的协议。
OOPSLA 6(OOPSLA1)2022匹配度 3/10引用 2并发、并行与内存模型程序合成程序分析与抽象解释
P2 A symmetric protocol to establish service level agreements
一种建立服务级别协议的对称协议
提出一种双方动态协商服务等级的对称协议，并用模态公式与行为归约验证其正确性。
LMCS vol.Volume 16, Issue 32020匹配度 3/10引用 2并发、并行与内存模型形式语义
P2 Reorder Pointer Flow in Sound Concurrency Bug Prediction
在可靠的并发缺陷预测中重排指针流
提出流敏感并发指针分析 ConPTA，并据此实现缺陷预测工具 Eagle，通过主动重排指针流检测四类并发指针缺陷。
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 3/10引用 1并发、并行与内存模型程序分析与抽象解释
P2 CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory
CBMC-SSM：带符号影子内存的 C 程序有界模型检测
为 CBMC 实现符号影子内存扩展，并通过代码翻译构造数据竞争分析器。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 3/10引用 1程序验证并发、并行与内存模型
P2 A Modular Static Cost Analysis for GPU Warp-Level Parallelism
面向 GPU Warp 级并行的模块化静态代价分析
提出首个可精确处理线程分歧的 GPU warp 级并行关系代价静态分析，支持资源度量与代价关系参数化，并实现 Rocq 验证工具 Pico。
POPL 10(POPL)2026匹配度 3/10引用 1程序分析与抽象解释并发、并行与内存模型
P2 All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
一人为大家，大家为一人：利用并行程序内部确定性的程序逻辑
提出利用内部确定性简化并行程序验证的程序逻辑，并在 Rocq/Iris 中机器化验证。
POPL 10(POPL)2026匹配度 3/10引用 1程序验证并发、并行与内存模型
P2 Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
在松弛内存分离逻辑中验证无锁遍历
首次在松弛内存一致性下形式验证无锁链表、跳表及跳表优先队列，提出逐键线性化历史规约与 shadowed-by 关系。
PLDI 9(PLDI)2025匹配度 3/10引用 1程序验证并发、并行与内存模型
P2 Probabilistic Refinement Session Types
概率精化会话类型
提出概率精化会话类型 PReST，以符号化精化推理支持非常量概率的并发概率程序验证。
PLDI 9(PLDI)2025匹配度 3/10引用 1类型系统并发、并行与内存模型
P2 Proving Correctness of Parallel Implementations of Transition System Models
证明转移系统模型的并行实现正确性
提出基于模拟关系的方法，证明 actor/active object 并行实现相对于转移系统规范的正确性。
TOPLAS 46(3)2024匹配度 3/10引用 1程序验证并发、并行与内存模型
P2 CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
CQS：一个形式化验证的公平且可中止同步框架
提出 CQS，用队列算法与 Coq/Iris 形式化证明实现公平、可中止同步原语，并在 JVM/Kotlin 协程中落地。
PLDI 7(PLDI)2023匹配度 3/10引用 1并发、并行与内存模型程序验证
P2 Interprocedural Context-Unbounded Program Analysis Using Observation Sequences
使用观察序列的过程间上下文无界程序分析
提出观察序列验证范式，以允许的线程上下文切换数为资源参数，实现可证明上下文无界安全性的过程间并发程序可达性分析。
TOPLAS 42(4)2020匹配度 3/10引用 1程序验证并发、并行与内存模型
P2 A Denotational Semantics for SPARC TSO
SPARC TSO 的一种指称语义
为 SPARC TSO 弱内存模型提出可组合的 pomsets 指称语义，并证明其相对公理语义可靠且完备。
LMCS vol.Volume 15, Issue 22019匹配度 3/10引用 1形式语义并发、并行与内存模型
P2 A Design Space Exploration of Async/Await
Async/Await 的设计空间探索
系统梳理 straight-line asynchrony 的九维设计空间，揭示看似相同的 async/await 在语义上的分歧。
OOPSLA 10(OOPSLA2)2026匹配度 3/10语言设计与特性并发、并行与内存模型
P2 LVing: A Vulnerability Detection and Visualization Platform for Rust
LVing：面向 Rust 的漏洞检测与可视化平台
提出 LVing，基于 LLVM IR 与代码属性图的 Rust 漏洞检测和交互式可视化平台，可发现并发漏洞。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10程序分析与抽象解释并发、并行与内存模型
P2 Spinner: Detecting Locking Violations in the eBPF Runtime
Spinner：检测 eBPF 运行时中的锁违规
提出静态分析工具 Spinner，检测 eBPF 运行时中因上下文混淆与嵌套程序递归调用导致的锁违规。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10程序分析与抽象解释并发、并行与内存模型
P2 SpecChecker-Int: An Extensible Concurrency Bugs Detection Tool for Interrupt-driven Embedded Software
SpecChecker-Int：一种面向中断驱动嵌入式软件的可扩展并发缺陷检测工具
提出可扩展工具 SpecChecker-Int，将并发缺陷建模为关键交错序列，并用抢占点选择缩减路径探索空间。
FSE Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering2025匹配度 3/10程序分析与抽象解释并发、并行与内存模型
P2 Reduce Dependence for Sound Concurrency Bug Prediction
减少依赖以实现可靠的并发缺陷预测
提出必要一致读事件（NRE）与混合分析算法，用静态语义精化读依赖，在不牺牲可靠性的前提下扩大线程交错空间，发现更多并发缺陷。
ICSE 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)2025匹配度 3/10并发、并行与内存模型程序分析与抽象解释
P2 Robustness against the C/C++11 Memory Model
对 C/C++11 内存模型的鲁棒性
提出一种证明程序对 C/C++11 内存模型具有鲁棒性的方法，从而可在顺序一致性语义下推理且不牺牲性能。
ISSTA Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis2024匹配度 3/10并发、并行与内存模型程序验证
P2 Characterizing Flaky Tests in Node.js Applications
Node.js 应用中不稳定测试的特征分析
对 7 个 Node.js 应用的 87 个不稳定测试开展实证研究，归纳五类非确定性根因，指出现有事件竞争检测方法不足。
ASE 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)2023匹配度 3/10测试、调试与修复并发、并行与内存模型
P2 Static executes-before analysis for event driven programs
事件驱动程序的静态 executes-before 分析
提出基于任务后图的静态分析，精确计算事件驱动程序中任务间的 executes-before 关系，并用于提升数据竞态检测精度。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 3/10程序分析与抽象解释并发、并行与内存模型
P2 The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
帝国的幽灵：从基于交错的证明中提取模块化
将并发程序基于交错的正确性证明自动转换为 Owicki-Gries 风格线程模块化证明，并合成 ghost 变量以压缩证明。
POPL 10(POPL)2026匹配度 3/10程序验证并发、并行与内存模型
P2 RAT-CAT-SAT: Model Checking Memory Consistency Models
RAT-CAT-SAT：内存一致性模型的模型检测
提出 RAT-CAT-SAT，用关系逻辑可满足性与循环证明系统对 CAT 内存一致性模型进行模型检测。
OOPSLA 10(OOPSLA1)2026匹配度 3/10并发、并行与内存模型程序验证逻辑与自动机
P2 Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing
Mixtris：面向混合选择多方消息传递的机械化高阶分离逻辑
提出首个混合选择多方消息传递的高阶分离逻辑 Mixtris，并在 Rocq/Iris 中机械验证其可靠性与实例。
OOPSLA 10(OOPSLA1)2026匹配度 3/10程序验证并发、并行与内存模型定理证明与证明工程
P2 Fast Atomicity Monitoring
快速原子性监控
提出 AtomSanitizer，以 O(nk²) 时间流式检测冲突可串行化，并首次支持低锁并发运行时监控。
PLDI 10(PLDI)2026匹配度 3/10并发、并行与内存模型测试、调试与修复
P2 A Separation Logic for Parallel Time Complexity with Work and Span Credits
一种带 work 与 span credit 的并行时间复杂度分离逻辑
提出 Parcas，用 work credit 与 span credit 在并发分离逻辑中模块化验证 fork-join 程序的并行时间上界，并在 Rocq/Iris 中机器化。
ICFP 10(ICFP)2026匹配度 3/10程序验证并发、并行与内存模型
P2 TSO Games -- On the decidability of safety games under the total store order semantics (extended LMCS version with appendix)
TSO 博弈——总存储序语义下安全博弈的可判定性（含附录的扩展 LMCS 版本）
将 TSO 语义扩展为回合制双人安全博弈，并给出不同缓冲区刷新责任下可判定性的完整图谱。
LMCS vol.Volume 21, Issue 32025匹配度 3/10并发、并行与内存模型逻辑与自动机
P2 Towards Verifying Crash Consistency
迈向崩溃一致性验证
提出 CrashLang 语言与类型系统，保证良类型数据结构实现崩溃一致，并实现编译器验证五个基准。
OOPSLA 9(OOPSLA2)2025匹配度 3/10类型系统并发、并行与内存模型
P2 A Refinement Methodology for Distributed Programs in Rust
面向 Rust 分布式程序的精化方法论
提出自底向上精化方法，用局部归纳不变式关联抽象模型与 Rust 实现，并可复用现成验证工具。
OOPSLA 9(OOPSLA2)2025匹配度 3/10程序验证并发、并行与内存模型
P2 Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
非单调资源度量下并发程序的最坏情况输入生成
首个面向并发程序、在内存等非单调资源度量下可靠的（相对完备的）最坏情况输入生成算法，结合资源标注会话类型与符号执行。
LMCS vol.Volume 20, Issue 42024匹配度 3/10并发、并行与内存模型程序分析与抽象解释
P2 Pipelines and Beyond: Graph Types for ADTs with Futures
流水线及其之外：面向带 future 的代数数据类型的图类型
提出支持 future 与递归数据类型近乎任意组合的图类型系统，可静态推断并证明可靠性。
POPL 8(POPL)2024匹配度 3/10类型系统并发、并行与内存模型
P2 Inductive Diagrams for Causal Reasoning
面向因果推理的归纳图
提出归纳式因果分离图（CSD），用路径依赖类型形式化 happens-before，并在 Agda 中验证逻辑时钟条件。
OOPSLA 8(OOPSLA1)2024匹配度 3/10形式语义定理证明与证明工程并发、并行与内存模型
P2 AtomiS: Data-Centric Synchronization Made Practical
AtomiS：面向实用的以数据为中心的同步
提出 AtomiS，通过接口与字段类型限定和静态分析自动生成并发控制，使数据中心同步更实用。
OOPSLA 7(OOPSLA2)2023匹配度 3/10并发、并行与内存模型程序分析与抽象解释编译与代码生成
P2 Mending Fences with Self-Invalidation and Self-Downgrade
用自失效与自降级修补栅栏
为采用自失效/自降级的一致性协议建立形式语义，并给出面向安全性的最小代价栅栏插入方法。
LMCS vol.Volume 14, Issue 12018匹配度 3/10并发、并行与内存模型程序验证
P2 Overlap Communication with Dependent Computation via Decomposition in Large Deep Learning Models
在大规模深度学习模型中通过分解重叠通信与依赖计算
提出将通信集合与依赖计算操作分解为细粒度操作并重叠执行的技术，隐藏数据传输延迟，提升大规模模型系统吞吐。
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 12022匹配度 2/10引用 127机器学习与程序语言并发、并行与内存模型
P2 Less is more: multiparty session types revisited
少即是多：多方会话类型再探
提出更简单且更通用的多方会话类型理论，去除全局类型与二元对偶，修复类型安全证明缺陷，并支持可判定类型检查与活性保证。
POPL 3(POPL)2019匹配度 2/10引用 104并发、并行与内存模型类型系统
P2 Don’t Sit on the Fence
不要坐在栅栏上
提出面向大型代码库的内存栅栏自动放置技术，以精度换可扩展性，并实现为 musketeer 工具。
TOPLAS 39(2)2017匹配度 2/10引用 91并发、并行与内存模型程序分析与抽象解释
P2 Manifest sharing with session types
会话类型中的 Manifest 共享
将共享机制引入会话类型语言，通过线性/共享分层与模态算子，在保持会话保真性的同时允许共享进程竞争导致的死锁。
ICFP 1(ICFP)2017匹配度 2/10引用 83类型系统并发、并行与内存模型
P2 Understanding Real-World Concurrency Bugs in Go
理解 Go 语言中的真实世界并发缺陷
首次系统研究真实 Go 程序中的并发缺陷，揭示过半缺陷源于 Go 特有机制，并评估修复与检测工具。
ASPLOS Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems2019匹配度 2/10引用 78并发、并行与内存模型测试、调试与修复
P2 PMTest
PMTest：面向持久内存崩溃一致性软件的测试框架
提出灵活且快速的 PMTest 框架，用两个基本检查器检测持久内存软件的崩溃一致性缺陷。
ASPLOS Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems2019匹配度 2/10引用 73测试、调试与修复并发、并行与内存模型
P2 Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
精确预测分析：发现 MPI 程序中的通信死锁
提出基于偏序与命题编码的 MPI 通信死锁预测分析方法，并实现 MOPPER 工具，可扩展地检测单路径程序死锁。
TOPLAS 39(4)2017匹配度 2/10引用 68并发、并行与内存模型程序验证
P2 RustBelt meets relaxed memory
RustBelt 遇上宽松内存
通过同步幽灵状态，将 RustBelt 的 Rust 语义健全性证明扩展到宽松内存，并发现 Arc 库中的数据竞争。
POPL 4(POPL)2019匹配度 2/10引用 66程序验证并发、并行与内存模型定理证明与证明工程
P2 A Formal Analysis of the NVIDIA PTX Memory Consistency Model
NVIDIA PTX 内存一致性模型的形式化分析
对 NVIDIA PTX 内存模型进行公理化建模、Alloy 测试与 Coq 机器验证，证明其可作为 CUDA 等语言的可靠编译目标。
ASPLOS Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems2019匹配度 2/10引用 61并发、并行与内存模型定理证明与证明工程
P2 Towards Practical Default-On Multi-Core Record/Replay
面向实用的默认开启多核记录/重放
提出 Castor 多核记录/重放系统，实现持续低且可预测的开销，使默认开启记录与重放成为可能。
ASPLOS Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems2017匹配度 2/10引用 61运行时与内存管理测试、调试与修复并发、并行与内存模型
P2 Persistency semantics of the Intel-x86 architecture
Intel-x86 架构的持久性语义
首次形式化 Intel-x86 的持久性语义 Px86，给出操作式与声明式定义并证明二者等价。
POPL 4(POPL)2019匹配度 2/10引用 61形式语义并发、并行与内存模型
P2 Grounding thin-air reads with event structures
用事件结构为 thin-air reads 奠定基础
提出基于事件结构的并发内存语义，禁止 thin-air reads，并证明其与 promising 语义等价且更易扩展。
POPL 3(POPL)2019匹配度 2/10引用 59并发、并行与内存模型形式语义
P2 Bridging the gap between programming languages and hardware weak memory models
弥合编程语言与硬件弱内存模型之间的鸿沟
提出中间弱内存模型 IMM，将并发语言到 POWER/ARM 的编译正确性证明模块化，并在 Coq 中机器验证。
POPL 3(POPL)2019匹配度 2/10引用 55并发、并行与内存模型编译与代码生成
P2 Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures
在 Go 中使用角色参数化会话类型进行分布式编程：面向动态实例化通信结构的静态类型端点 API
提出角色参数化多体会话类型理论，并为 Go 生成静态类型端点 API，以安全实现动态参与者协议。
POPL 3(POPL)2019匹配度 2/10引用 55并发、并行与内存模型类型系统
P2 AdaPipe: Optimizing Pipeline Parallelism with Adaptive Recomputation and Partitioning
AdaPipe：通过自适应重计算与分区优化流水线并行
提出 AdaPipe，通过自适应重计算与灵活阶段划分，优化流水线并行的内存与计算均衡，加速大模型训练。
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32024匹配度 2/10引用 54机器学习与程序语言并发、并行与内存模型
P2 ProRace
ProRace：面向生产运行的实用数据竞争检测器
ProRace 通过 PMU 指令采样与离线重建未采样访存，实现生产可用的低开销动态数据竞争检测。
ASPLOS Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems2017匹配度 2/10引用 50并发、并行与内存模型程序分析与抽象解释
P2 Safe Automated Refactoring for Intelligent Parallelization of Java 8 Streams
面向 Java 8 Stream 智能并行化的安全自动重构
提出基于数据顺序与类型状态分析的安全自动重构，将顺序 Stream 安全并行化或去并行化。
ICSE 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE)2019匹配度 2/10引用 48程序分析与抽象解释并发、并行与内存模型
P2 Automata for Specifying and Orchestrating Service Contracts
用于服务契约规约与编排的自动机
用自动机形式化描述服务契约，并在同步/异步多主体组合中构造编排器以保证请求满足。
LMCS vol.Volume 12, Issue 42017匹配度 2/10引用 46逻辑与自动机并发、并行与内存模型
P2 Actris: session-type based reasoning in separation logic
Actris：分离逻辑中基于会话类型的推理
提出 Actris，将基于会话类型的一等协议机制融入并发分离逻辑，用 Coq 机器化验证消息传递程序的功能正确性。
POPL 4(POPL)2019匹配度 2/10引用 44程序验证并发、并行与内存模型定理证明与证明工程
P2 Armed Cats
武装的猫：Arm 一致性模型的形式化建模
综述 Arm 用 cat 语言形式化并发一致性模型的工作，含混合大小访问扩展、等价表述及 x86 验证。
TOPLAS 43(2)2021匹配度 2/10引用 43并发、并行与内存模型形式语义
P2 Honesty by Typing
通过类型系统保证诚实性
提出面向契约进程演算的类型系统，保证可类型化进程在所有上下文中诚实，并给出可判定的类型推断。
LMCS vol.Volume 12, Issue 42017匹配度 2/10引用 40类型系统并发、并行与内存模型
P2 FlexSP: Accelerating Large Language Model Training via Flexible Sequence Parallelism
FlexSP：通过灵活的序列并行加速大语言模型训练
提出异构自适应序列并行 FlexSP，按序列长度动态选择散射策略，加速长上下文 LLM 训练。
ASPLOS Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22025匹配度 2/10引用 37机器学习与程序语言并发、并行与内存模型
P2 Frightening Small Children and Disconcerting Grown-ups
吓坏小孩，让大人不安
为 Linux 内核内存一致性提供可执行的 cat 形式模型，并用 herd 验证，形式化并证明 RCU 定律。
ASPLOS Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems2018匹配度 2/10引用 37并发、并行与内存模型形式语义
P2 Simuliris: a separation logic framework for verifying concurrent program optimizations
Simuliris：一个用于验证并发程序优化的分离逻辑框架
提出 Simuliris，首个在公平调度下证明利用未定义行为的并发程序变换保持终止的模拟技术。
POPL 6(POPL)2022匹配度 2/10引用 33程序验证并发、并行与内存模型
P2 Chronos: Efficient Speculative Parallelism for Accelerators
Chronos：面向加速器的高效推测并行
提出 SLOT 执行模型与 Chronos 框架，使加速器无需缓存一致性即可高效支持推测并行。
ASPLOS Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems2020匹配度 2/10引用 32语言与体系结构并发、并行与内存模型
P2 SteelCore: an extensible concurrent separation logic for effectful dependently typed programs
SteelCore：面向带效果依赖类型程序的可扩展并发分离逻辑
在 F* 的效果化依赖类型论中为并发分离逻辑给出语义，并据此构建可扩展的并发验证库。
ICFP 4(ICFP)2020匹配度 2/10引用 31程序验证并发、并行与内存模型
P2 Controlled concurrency testing via periodical scheduling
基于周期性调度的受控并发测试
提出周期性调度的受控并发测试技术 Period，系统探索线程交错以更高效检测并发缺陷。
ICSE Proceedings of the 44th International Conference on Software Engineering2022匹配度 2/10引用 29测试、调试与修复并发、并行与内存模型
P2 Gradual session types
渐进会话类型
提出 GradualGV，将动态类型与 cast 引入函数式会话类型系统 GV，统一静态与动态会话处理并保证类型、通信与 blame 安全。
ICFP 1(ICFP)2017匹配度 2/10引用 29类型系统并发、并行与内存模型
P2 Sound and efficient concurrency bug prediction
可靠且高效的并发缺陷预测
提出 SeqCheck，可靠判定事件序列能否按指定顺序发生以预测并发缺陷，并在双线程轨迹上完备。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 2/10引用 28测试、调试与修复并发、并行与内存模型
P2 CloudRaid: hunting concurrency bugs in the cloud via log-mining
CloudRaid：通过日志挖掘猎捕云中的并发缺陷
提出 CloudRaid，通过挖掘历史日志翻转测试不足的消息顺序，自动检测云系统中的分布式并发缺陷。
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 2/10引用 28测试、调试与修复并发、并行与内存模型
P2 Detecting Isolation Bugs via Transaction Oracle Construction
通过事务预言机构造检测 DBMS 隔离性缺陷
提出 Troc，将事务拆为独立语句并按声称隔离级别构造视图，通过执行分歧检测 DBMS 隔离性缺陷。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 2/10引用 27测试、调试与修复并发、并行与内存模型
P2 C4: verified transactional objects
C4：已验证的事务对象
提出 C4 形式验证框架，统一证明事务对象与 STM 库的线性化与可串行化，并在 Coq 中机器化。
OOPSLA 6(OOPSLA1)2022匹配度 2/10引用 27程序验证并发、并行与内存模型定理证明与证明工程
P2 Atomicity Checking in Linear Time using Vector Clocks
使用向量时钟的线性时间原子性检查
提出基于向量时钟的单遍线性时间算法 AeroDrome，在线检测冲突可串行化违反以实现原子性检查。
ASPLOS Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems2020匹配度 2/10引用 26并发、并行与内存模型程序分析与抽象解释
P2 Precise subtyping for asynchronous multiparty sessions
异步多参与方会话的精确子类型
首次形式化异步多方会话的精确子类型，并证明其可靠且完备，实现安全进程替换与异步消息优化。
POPL 5(POPL)2021匹配度 2/10引用 26类型系统并发、并行与内存模型
P2 Taming x86-TSO persistency
驯服 x86-TSO 持久性
为 x86-TSO 非易失内存建立等价持久性模型，并给出到 x86 的健全映射与数据竞争自由保证。
POPL 5(POPL)2021匹配度 2/10引用 26形式语义并发、并行与内存模型
P2 What’s Decidable About Causally Consistent Shared Memory?
因果一致共享内存的可判定性是什么？
本文证明两类因果一致共享内存下有限状态并发程序的安全性验证可判定，并给出基于有损操作语义的判定方法。
TOPLAS 44(2)2022匹配度 2/10引用 25并发、并行与内存模型程序验证
P2 Tracing where IoT data are collected and aggregated
追踪 IoT 数据的收集与聚合位置
提出 IoT-LySa 进程演算及静态分析，追踪 IoT 数据来源、聚合与流动，以支持安全等非功能性质验证。
LMCS vol.Volume 13, Issue 32017匹配度 2/10引用 25并发、并行与内存模型程序分析与抽象解释安全与隐私
P2 Flaky test detection in Android via event order exploration
Android 中通过事件顺序探索检测 flaky test
提出 FlakeScanner，通过探索事件顺序检测 Android 应用中的 flaky test，并发布 FlakyAppRepo 数据集。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 2/10引用 24测试、调试与修复并发、并行与内存模型
P2 Deep Dive into ZGC: A Modern Garbage Collector in OpenJDK
深入剖析 ZGC：OpenJDK 中的现代垃圾收集器
对 OpenJDK ZGC 做高层设计解析，并用 SPIN 模型解释 mutator 与 GC 线程的并发竞争及解决。
TOPLAS 44(4)2022匹配度 2/10引用 24运行时与内存管理并发、并行与内存模型
P2 Cosmo: a concurrent separation logic for multicore OCaml
Cosmo：多核 OCaml 的并发分离逻辑
为多核 OCaml 的弱内存模型构建分层并发分离逻辑 Cosmo，支持从底层到高层的程序验证。
ICFP 4(ICFP)2020匹配度 2/10引用 24程序验证并发、并行与内存模型
P2 Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
扩展 Intel-x86 一致性与持久性：形式化 Intel-x86 内存类型与非临时存储的语义
将 Intel-x86 一致性/持久性语义扩展到非临时写、不可缓存、写合并和写穿内存类型，并证明操作式与声明式模型等价。
POPL 6(POPL)2022匹配度 2/10引用 23并发、并行与内存模型形式语义
P2 PFix: fixing concurrency bugs based on memory access patterns
PFix：基于内存访问模式修复并发缺陷
从失败相关的内存访问模式推断锁策略，自动修复 Java 并发缺陷。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 2/10引用 22测试、调试与修复并发、并行与内存模型
P2 Who goes first? detecting go concurrency bugs via message reordering
谁先执行？通过消息重排序检测 Go 并发缺陷
提出通过消息重排序来检测 Go 程序中 channel 相关并发缺陷的方法。
ASPLOS Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems2022匹配度 2/10引用 21并发、并行与内存模型测试、调试与修复
P2 Verifying observational robustness against a c11-style memory model
针对 C11 风格内存模型验证观测鲁棒性
提出观测鲁棒性，将 C11 风格内存模型下的并发程序鲁棒性验证归约为顺序一致性下的可达性问题。
POPL 5(POPL)2021匹配度 2/10引用 21并发、并行与内存模型程序验证
P2 Reductions for safety proofs
面向安全性证明的归约
提出基于程序上下文的两类可靠程序归约，利用步骤可交换性简化并发程序安全性证明与自动验证。
POPL 4(POPL)2019匹配度 2/10引用 21程序验证并发、并行与内存模型
P2 Symbolic verification of message passing interface programs
消息传递接口（MPI）程序的符号验证
提出 MPI-SV，首个基于符号执行并可自动验证含非阻塞操作的 MPI 程序的工具。
ICSE Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering2020匹配度 2/10引用 20程序验证并发、并行与内存模型
P2 Effectiveness and challenges in generating concurrent tests for thread-safe classes
面向线程安全类的并发测试生成：有效性与挑战
对自动生成线程安全类并发测试的现有工具进行独立实证评估，发现仅17%的并发故障被检出。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 2/10引用 20测试、调试与修复并发、并行与内存模型
P2 The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
分号泄漏：面向松弛内存并发的组合式语义依赖
通过前置条件和谓词变换器族，为松弛内存并发中的顺序组合提供组合式语义。
POPL 6(POPL)2022匹配度 2/10引用 20并发、并行与内存模型形式语义
P2 Directed Homotopy in Non-Positively Curved Spaces
非正曲率空间中的有向同伦
本文用预立方集合为互斥锁并发程序建模，引入非正曲率概念，证明有向同伦与无向同伦在特定有向路径上一致。
LMCS vol.Volume 16, Issue 32020匹配度 2/10引用 20并发、并行与内存模型形式语义
P2 Greybox Fuzzing for Concurrency Testing
并发测试的灰盒模糊测试
提出利用 reads-from 关系引导偏置随机搜索的并发测试灰盒模糊方法，高效发现并发缺陷。
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22024匹配度 2/10引用 19测试、调试与修复并发、并行与内存模型
P2 A tree clock data structure for causal orderings in concurrent executions
并发执行中因果序的树时钟数据结构
提出树时钟替代向量时钟计算并发执行的因果序，使 join/copy 代价与修改条目数成正比，并证明其在 happens-before 下的渐进最优性。
ASPLOS Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems2022匹配度 2/10引用 19并发、并行与内存模型
P2 Perspective
Perspective：推测式自动并行化框架
提出 Perspective 推测式自动并行化框架，以接近非推测方法的效率实现 DOALL 并行化。
ASPLOS Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems2020匹配度 2/10引用 19编译与代码生成并发、并行与内存模型
P2 Disentanglement in nested-parallel programs
嵌套并行程序中的解纠缠
提出嵌套并行程序的内存性质“解纠缠”，并据此设计内存管理技术以提升效率与可扩展性。
POPL 4(POPL)2019匹配度 2/10引用 19并发、并行与内存模型运行时与内存管理
P2 Yashme: detecting persistency races
Yashme：检测持久性竞态
提出持久性竞态这一崩溃一致性缺陷，并实现首个检测器 Yashme，在持久内存基准中发现 26 个真实竞态。
ASPLOS Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems2022匹配度 2/10引用 18并发、并行与内存模型测试、调试与修复