Discourje：Clojure 中通信协议的运行时验证——终于实现活性（技术报告）
Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last (Technical Report)
AI总结：
本文扩展了基于动态多方会话类型的 Clojure 运行时验证库 Discourje，使其在原有安全性违规检测能力之外，新增了对活性（通信无死锁）违规的检测能力。
摘要：
多方会话类型（MPST）是一种使并发编程更简单的形式化方法。其思想是利用类型检查来自动证明实现相对于规范的安全性（协议合规性）和活性（通信无死锁）。Discourje 是一个现有的基于动态 MPST 的 Clojure 通信协议运行时验证库。Discourje 的原始版本只能检测安全性违规。在本文中，我们提出了 Discourje 的一个扩展，使其也能检测活性违规。
英文摘要：
Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (communication deadlock freedom) of implementations relative to specifications. Discourje is an existing run-time verification library for communication protocols in Clojure, based on dynamic MPST. The original version of Discourje can detect only safety violations. In this paper, we present an extension of Discourje to detect also liveness violations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
