paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis

Oven:使用合成行为类型分析保障 Scala 中通信协议的安全性与活性
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 2/10 · 该论文属于静态分析与类型系统在并发通信协议中的应用,与用户画像中PL与AI/LLM交叉、浮点程序分析、贝叶斯程序分析等核心方向均无直接关联。虽然它兼具理论形式化和工程实现,可能对广义PL静态分析有参考价值,但并非当前追踪的问题。引用 3 inbox
Francisco Ferreira, Sung-Shik Jongmans
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出 Oven:首个基于合成行为类型分析、在 Scala 中保障并发通信协议安全性与活性的实用工具集。

并发程序中线程间通信协议的安全性与活性难以保证,现有行为类型分析的表达力亦有局限。作者提出 Oven:一个 Scala 工具集,建立在其新近提出的合成行为类型(synthetic behavioural type analysis)理论基础上,用于在 Scala 现有类型系统中编码新的合成行为类型规则,从而检查线程间通信协议是否符合规约。论文介绍了 Oven 的用法,总结了设计与实现,并讨论了表达力的初步评估;结果表明,Oven 相较于两个最先进的工具具有改进,首次提供了其实用性与表达力优势的证据。

问题
如何在 Scala 并发程序中保证线程间通信协议的安全性与活性,并提升现有行为类型分析的表达力。
方法
Oven 工具集基于合成行为类型分析,将其新类型规则编码进 Scala 现有类型系统,用于协议检查;论文说明其用法、设计与实现。
评估
通过表达力的初步评估,并与两个 state-of-the-art 工具比较,获得 Oven 更优的首批证据。
原文摘要(Abstract)

We present Oven: a toolset to assure safety and liveness of communication protocols among threads in concurrent programs in Scala. Oven is the first practical toolset that is built on top of new theoretical foundations of synthetic behavioural type analysis, recently developed by us to improve the expressiveness of existing work. We explain Oven's usage, summarise its design and implementation (main challenge: how to encode the new synthetic behavioural typing rules in Scala's existing type system), and discuss a preliminary evaluation of expressiveness (the results provide first evidence that Oven is an improvement over two state-of-the-art tools).

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{FerreiraJ23,
  title = {Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis},
  author = {Francisco Ferreira and Sung-Shik Jongmans},
  booktitle = {ISSTA},
  year = {2023},
  doi = {10.1145/3597926.3604926}
}