Title: Local Search for SMT on Linear Integer Arithmetic 

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

Time: 7月1日（周五） 09:30-11:00

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

线上（腾讯会议 597-336-185）

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