一句话：提出基于行为类型的静态验证框架，用于检查 Go 通道消息传递程序的并发正确性。
Go 因将系统编程与并发结合而在工业界广泛使用，其通道通信和轻量线程源自 CCS、CSP 等进程演算，为并发软件提供独特结构。然而 Go 生态几乎缺乏保证消息传递并发程序正确性的支持。本文提出一个静态验证框架，利用行为类型（behavioural types）对 Go 中基于通道的消息传递程序进行建模与静态检查，目标是对这类并发程序的正确性提供保证。给出的摘要仅概述动机、定位与方法，未报告具体实现细节、案例研究或实验评估结果。
The Go programming language has been heavily adopted in industry as a language that efficiently combines systems programming with concurrency. Go's concurrency primitives, inspired by process calculi such as CCS and CSP, feature channel-based communication and lightweight threads, providing a distinct means of structuring concurrent software. Despite its popularity, the Go programming ecosystem offers little to no support for guaranteeing the correctness of message-passing concurrent programs.
@inproceedings{paperbot4509,
title = {A static verification framework for message passing in Go using behavioural types},
author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida},
booktitle = {ICSE},
year = {2018},
doi = {10.1145/3180155.3180157}
}