软件所团队获第十六届国际可满足性模理论比赛整数差分逻辑组冠军
来源：软件研究所 时间：2021年08月17日
近日，形式化验证会议CAV 2021公布了第十六届国际可满足性模理论比赛（SMT-COMP 2021）结果。中国科学院软件研究所计算机科学国家重点实验室研究员蔡少伟团队研发的求解器获整数差分逻辑（QF_IDL）组冠军，这是中国团队首次在SMT-COMP中获得冠军。
可满足性模理论问题（SMT）是特定背景理论下的一阶逻辑判定问题，是形式化验证的基础引擎。整数差分逻辑理论的SMT可以自然地描述时序相关的问题，广泛应用于时序系统验证、偏序数据结构的硬件模型检测和稳态模型计算。
在SMT-COMP 2021中，QF_IDL组的参赛队伍包括美国斯坦福大学、美国爱荷华大学、德国弗莱堡大学、微软研究院、国际斯坦福研究所、法国国家信息与自动化研究所等高校及科研院所。软件所团队创新性地设计了结合DPLL(T)和随机搜索方法的混合方法，打破了传统SMT求解器框架，在强数值约束算例中取得显著效果，最终在QF_IDL理论的Single query和Model validation赛道上都取得了第一名。