Grigore Roșu 是 UIUC / Runtime Verification 的计算机科学教授兼创始人。本期讨论结合形式化规格、LLM 代码迁移与形式化证明发现内核漏洞的方法。
Grigore Roșu is affiliated with UIUC / Runtime Verification (计算机科学教授兼创始人). This episode discusses combining formal specifications, LLM-assisted code translation, and formal proofs to find kernel vulnerabilities.
介绍来源
原发布方节目与人物署名 · 核对于 2026-10-18。依据原节目发布时的介绍。
