軟件所團(tuán)隊獲第十六屆國際可滿足性模理論比賽整數(shù)差分邏輯組冠軍
來源：軟件研究所 時間：2021年08月17日
近日，形式化驗(yàn)證會議CAV 2021公布了第十六屆國際可滿足性模理論比賽（SMT-COMP 2021）結(jié)果。中國科學(xué)院軟件研究所計算機(jī)科學(xué)國家重點(diǎn)實(shí)驗(yàn)室研究員蔡少偉團(tuán)隊研發(fā)的求解器獲整數(shù)差分邏輯（QF_IDL）組冠軍，這是中國團(tuán)隊首次在SMT-COMP中獲得冠軍。
可滿足性模理論問題（SMT）是特定背景理論下的一階邏輯判定問題，是形式化驗(yàn)證的基礎(chǔ)引擎。整數(shù)差分邏輯理論的SMT可以自然地描述時序相關(guān)的問題，廣泛應(yīng)用于時序系統(tǒng)驗(yàn)證、偏序數(shù)據(jù)結(jié)構(gòu)的硬件模型檢測和穩(wěn)態(tài)模型計算。
在SMT-COMP 2021中，QF_IDL組的參賽隊伍包括美國斯坦福大學(xué)、美國愛荷華大學(xué)、德國弗萊堡大學(xué)、微軟研究院、國際斯坦福研究所、法國國家信息與自動化研究所等高校及科研院所。軟件所團(tuán)隊創(chuàng)新性地設(shè)計了結(jié)合DPLL(T)和隨機(jī)搜索方法的混合方法，打破了傳統(tǒng)SMT求解器框架，在強(qiáng)數(shù)值約束算例中取得顯著效果，最終在QF_IDL理論的Single query和Model validation賽道上都取得了第一名。