形式化验证、特别是模型检验技术是软件代码正确性保障不可或缺的重要途径。然而，软件代码状态空间复杂度极高，一方面，大规模程序状态空间快速爆炸，难以有效遍历，另一方面，复杂程序特征（浮点计算、非线性约束、第三方库函数调用等）约束问题难以求解。受相关问题制约，当前有界验证技术与工具的可处理问题规模和验证效率离实际问题需求之间存在巨大差距。因此，有效控制有界验证过程中的复杂性、研制满足工业界实际需求的代码有界验证技术和工具对于保障软件系统可靠性具有重要意义。

针对上述问题，卜磊老师带领同学们在有界验证框架下，从路径遍历与求解角度出发，不直接处理整体空间，而是从单条路径着手有效控制单次验证任务的复杂性，保证单条路径验证可计算，从而可对阈值内潜在路径进行遍历与求解，以完成有界验证的任务。在此基础上，进一步探索新型路径约束约剪技术，控制待验证路径空间。另一方面结合机器学习中约束优化技术，将正向路径约束求解转为无梯度优化问题，从而通过枚举-采样-确认方式进行求解，在复杂代码约束求解上效果显著。 

基于上述研究开发的嵌入式代码有界验证工具BRICK参加了国际软件验证大赛 SV-COMP 的ReachSafety赛道下的浮点数Floats分项赛。在这个分项赛中，BRICK求解数排名835分，排名第一，超过老牌验证工具CBMC（782），以及商用工具Veriabs（827）。 最值得一提的是BRICK耗时仅1000秒，而Veriabs耗时近18000秒，佐证了我们提出的基于路径遍历的验证思路的可行性与有效性。