[07-01] Local Search for SMT on Linear Integer Arithmetic

文章来源:  |  发布时间:2022-06-29  |  【打印】 【关闭

  

Title: Local Search for SMT on Linear Integer Arithmetic 

Speaker: 蔡少伟 研究员 计算机科学国家重点实验室

Time: 71日(周五) 09:30-11:00

Venue: 线下(中科院软件所5号楼三层 334报告厅)

线上(腾讯会议 597-336-185

 

Abstract: 该论文研发了线性整数算术SMT求解器LS-LIA,是首个支撑整数理论的随机搜索(Stochastic Local Search,简称SLS)求解器, 开创了SLS求解整数算术理论的先河。该求解器在标准测试集SMT-LIB上已经和前沿求解器包括Z3CVC5, Yices2, MathSAT5等达到竞争性和互补性的效果,并且在一些大规模样例上有突破性的表现。结合LS-LIAZ3的混合求解器可以在SMTLIB的测试集上做到目前最好效果。论文被CAV 2022录用。

Bio: 蔡少伟,中科院软件所计算机科学国家重点实验室研究员。个人网页:http://lcs.ios.ac.cn/~caisw/