近日,形式化验证顶级会议CAV 2021会议公布了第十六届国际可满足性模理论比赛(SMT-COMP 2021)比赛结果,中国科学院软件研究所(以下简称软件所)研究员蔡少伟带领团队研发的求解器荣获整数差分逻辑(QF_IDL)组冠军。这也是中国团队首次在SMT-COMP比赛中获得冠军。
“可满足性模理论问题(简称SMT)是特定背景理论下的一阶逻辑公式判定问题,是计算机科学和人工智能研究的核心问题之一,SMT求解器也是形式化验证的基础引擎。”蔡少伟表示。
会使用高级语言(如Pascal,C)编程的人,一定对可满足性问题不会感到陌生。在编程语言中,用于条件语句的布尔表达式由变量通过运算符以及“与”“或”“非”等逻辑连接符组合而成,给每个变量一个值,很容易判断出整个表达式是否为真。但反过来,给定一个表达式,是否能为每个变量找到值,使得整个表达式成真?这就是SMT的一种形式。
蔡少伟介绍,作为一种工具,SMT求解器在工业领域尤其是软硬件验证中具有广泛的应用价值。比如windows操作系统驱动程序的验证就用到了SMT求解器。
在此次SMT-COMP比赛中,蔡少伟团队自主研发了基于DPLL(T)和随机搜索混合的方法,打破了传统SMT求解器框架,在强数值约束的差分逻辑算例中取得了显著效果。
据悉,该研究团队长期从事约束求解器研究,进行SMT、SAT(命题逻辑可满足性问题)等计算机科学经典问题求解算法及工具的研发,并在相应领域国际大赛中多次获奖。其提出的约束求解技术和研制的SAT求解器已应用于华为公司的电路验证、腾讯地图优化、微软Azure云平台的虚拟机预配置和异常检测、以及美联邦通信委员会的频谱分配等项目中。(作者:胡珉琦)
责任编辑:kj005
文章投诉热线:156 0057 2229 投诉邮箱:29132 36@qq.com