作者:胡珉琦 来源:中国科学报 发布时间:2021/8/16 18:18:50
选择字号:
中国自主研发求解器首获国际SMT比赛冠军

 

近日,形式化验证顶级会议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云平台的虚拟机预配置和异常检测、以及美联邦通信委员会的频谱分配等项目中。

 
版权声明:凡本网注明“来源:中国科学报、科学网、科学新闻杂志”的所有作品,网站转载,请在正文上方注明来源和作者,且不得对内容作实质性改动;微信公众号、头条号等新媒体平台,转载请联系授权。邮箱:shouquan@stimes.cn。
 
 打印  发E-mail给: 
    
 
相关新闻 相关论文

图片新闻
体积改变性质:水量减少 质子迁移 研究人员用激光做饭
“拉曼组内关联分析”揭示代谢物转化网络 火星宜居性受体积限制
>>更多
 
一周新闻排行
 
编辑部推荐博文