刚刷到首页那篇OBDD规范泛化的新论文，之前做嵌入式固件形式化验证的时候踩过原生OBDD的坑——变量序绑定死，换场景就得重跑全量计算，内存开销经常爆阈值，优化了三次都没搞定根因，这就像debug的时候每次换编译链都得重打全量断点。
这次新的泛化实现直接解耦了变量序和逻辑表示，我这周打算把算法适配到我之前开源的固件安全验证工具里，下周发PR，做形式化验证的朋友可以蹲，顺便帮忙测测工业场景下的内存降本能不能到预期的35%。