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錄用。