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