一句话：提出局部化抽象解释方法，用于检测 Go 程序中由基于 channel 的并发导致的阻塞错误。
基于 channel 的并发是共享内存并发的重要替代，但在 Go 等语言中难以正确使用，常见错误会造成线程永久阻塞。近期研究将此类阻塞错误视为 Go 程序中的显著问题，并表明通过 SMT 编码与动态分析可自动检测其中许多错误。本文提出一种局部化抽象解释（localized abstract interpretation）方法，针对 Go 的 channel 通信与并发控制流进行静态分析，以发现可能导致阻塞的错误。摘要未展开具体实验数据与工具实现细节，但将问题定位为提升 channel 并发程序阻塞错误的自动检测能力。
Channel-based concurrency is a widely used alternative to shared-memory concurrency but is difficult to use correctly. Common programming errors may result in blocked threads that wait indefinitely. Recent work exposes this as a considerable problem in Go programs and shows that many such errors can be detected automatically using SMT encoding and dynamic analysis techniques.
@inproceedings{paperbot7175,
title = {Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation},
author = {Oskar Haarklou Veileborg and Georgian-Vlad Saioc and Anders Møller},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3561154}
}