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

时间：2022-06-29 分类：学术报告

Title: Local Search for SMT on Linear Integer Arithmetic
Speaker: 蔡少伟研究员计算机科学国家重点实验室
Time: 7月1日（周五） 10:00-12:00
Venue: 中科院软件所5号楼三层 334报告厅
Abstract: 该论文研发了线性整数算术SMT求解器LS-LIA，是首个支撑整数理论的随机搜索（Stochastic Local Search，简称SLS）求解器，开创了SLS求解整数算术理论的先河。该求解器在标准测试集SMT-LIB上已经和前沿求解器包括Z3，CVC5, Yices2, MathSAT5等达到竞争性和互补性的效果,并且在一些大规模样例上有突破性的表现。结合LS-LIA和Z3的混合求解器可以在SMTLIB的测试集上做到目前最好效果。论文被CAV 2022录用。
Bio: 蔡少伟，中科院软件所计算机科学国家重点实验室研究员。个人网页：http://lcs.ios.ac.cn/~caisw/