2019年10月10日至2020年2月22日，第9届国际软件代码验证工具竞赛 SV-COMP 2020 (9th Competition on Software Verification) 在线上举行，SEG团队开发的C代码验证工具BRICK在该竞赛的ReachSafety-Floats子项中表现优异，该工作参与同学包括硕士生闾乐成，本科生谢准一，以及已毕业硕士生李一超，该工作的指导老师是卜磊教授。

SV-COMP是展示自动软件验证领域最新前沿技术发展的验证工具竞赛之一，比赛为参赛的验证工具提供了统一的运行环境与基准用例，来公平准确地衡量每一款参赛工具的验证能力。

在ReachSafety-Floats子项中，基准用例侧重于浮点数计算，同时也包含数组、结构体和循环等复杂数据类型和程序结构。共计有来自中国、德国、印度、英国等国家研究院所的14款工具参加了该子项。本年度该子项一共466个案例，BRICK在所有工具中可解问题项上在466个案例上成功验证421个，仅落后第一名Veriabs 4个案例，排名第二。 然而我们在问题效率上显著优于其他所有工具（领先Veriabs 35 倍之多）。

另一方面，CBMC是由英国牛津大学开发的领域长期以来最知名验证工具，与CBMC相比 我们的工具可解决问题421高于CBMC 413， 而案例耗时上，CBMC耗时是我们的9倍之多。