土法炼钢 · 系统与基础设施

【操作系统百科】内核并发的形式化验证

2026-06-02 | os | #formal-verification #herd7 #litmus-test #cbmc #tla-plus

用 herd7 跑 litmus test、用 CBMC 检查有界模型、用 TLA+ 验证协议——内核并发代码的形式化验证实践。本文讲工具链、实际 bug 案例、与传统测试的权衡。