研究人员使用AI和行为规范语言在阿波罗11号制导计算机代码中发现了一个先前未记录的漏洞，涉及陀螺控制中的资源锁泄漏。尽管该代码经过广泛的历史审查，但通过形式化规范方法分析13万行汇编代码后仍发现了这一缺陷。这突显了现代验证工具即使在经过充分研究的遗留系统中也能发现缺陷。
背景
阿波罗制导计算机（AGC）代码自2003年起公开，是历史上被研究最多的代码库之一，但主要通过手动分析和模拟而非形式化验证方法进行研究。
- 来源
- Lobsters
- 发布时间
- 2026年4月13日 05:34
- 评分
- 7.0 / 10