一句话：将不正确性分离逻辑扩展到并发程序，提供参数化框架检测竞态、死锁和内存安全错误并保证真阳性。
不正确性分离逻辑（ISL）是一种欠近似推理理论，目标是证明组合式缺陷捕获器发现的是真实缺陷，但它只支持顺序程序。本文提出并发不正确性分离逻辑（CISL），将 ISL 扩展到并发程序的缺陷捕获。受 Views 工作启发，作者将 CISL 设计为参数化框架，可针对竞态检测、死锁检测和内存安全错误检测等场景实例化。对每个实例，CISL 元理论自动保证不正确性推理的可靠性，从而保证检测到的缺陷均为真阳性。
Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.
@article{paperbot1541,
title = {Concurrent incorrectness separation logic},
author = {Azalea Raad and Josh Berdine and Derek Dreyer and Peter W. O'Hearn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498695}
}