形式化验证 LLM 生成的代码（FATTW 2026, Lucas Cordeiro）
FATTW 2026 会议演讲（与 ASE 2026 联合举办）：LLM 负责猜测（不变量、契约、harness），证明引擎负责裁决（ESBMC/k-induction/Vampire）。以 310,531 个 C 程序基准、Test-Comp/SV-COMP 竞赛成绩和 AWS/NVIDIA/vLLM 生产代码漏洞为证据，论证『模型建议 + 证明引擎确认』的设计原则。
Topic
#ibmc
1 篇笔记
Topic
1 篇笔记
FATTW 2026 会议演讲（与 ASE 2026 联合举办）：LLM 负责猜测（不变量、契约、harness），证明引擎负责裁决（ESBMC/k-induction/Vampire）。以 310,531 个 C 程序基准、Test-Comp/SV-COMP 竞赛成绩和 AWS/NVIDIA/vLLM 生产代码漏洞为证据，论证『模型建议 + 证明引擎确认』的设计原则。