• <code id="mmi2u"><nav id="mmi2u"></nav></code>
  • <button id="mmi2u"></button>

    面向世界科技前沿,面向國家重大需求,面向國民經濟主戰場,率先實現科學技術跨越發展,率先建成國家創新人才高地,率先建成國家高水平科技智庫,率先建設國際一流科研機構。

    ——中國科學院辦院方針

    首頁 > 一線動態

    軟件所團隊獲第十六屆國際可滿足性模理論比賽整數差分邏輯組冠軍

    2021-08-17 軟件研究所
    【字體:

    語音播報

      近日,形式化驗證會議CAV 2021公布了第十六屆國際可滿足性模理論比賽(SMT-COMP 2021)結果。中國科學院軟件研究所計算機科學國家重點實驗室研究員蔡少偉團隊研發的求解器獲整數差分邏輯(QF_IDL)組冠軍,這是中國團隊首次在SMT-COMP中獲得冠軍。
      可滿足性模理論問題(SMT)是特定背景理論下的一階邏輯判定問題,是形式化驗證的基礎引擎。整數差分邏輯理論的SMT可以自然地描述時序相關的問題,廣泛應用于時序系統驗證、偏序數據結構的硬件模型檢測和穩態模型計算。 

      在SMT-COMP 2021中,QF_IDL組的參賽隊伍包括美國斯坦福大學、美國愛荷華大學、德國弗萊堡大學、微軟研究院、國際斯坦福研究所、法國國家信息與自動化研究所等高校及科研院所。軟件所團隊創新性地設計了結合DPLL(T)和隨機搜索方法的混合方法,打破了傳統SMT求解器框架,在強數值約束算例中取得顯著效果,最終在QF_IDL理論的Single query和Model validation賽道上都取得了第一名。

    打印 責任編輯:江澄

    掃一掃在手機打開當前頁

    © 1996 - 中國科學院 版權所有 京ICP備05002857號-1 京公網安備110402500047號 網站標識碼bm48000002

    地址:北京市西城區三里河路52號 郵編:100864

    電話: 86 10 68597114(總機) 86 10 68597289(總值班室)

    編輯部郵箱:casweb@cashq.ac.cn

  • © 1996 - 中國科學院 版權所有 京ICP備05002857號-1 京公網安備110402500047號 網站標識碼bm48000002

    地址:北京市西城區三里河路52號 郵編:100864

    電話: 86 10 68597114(總機) 86 10 68597289(總值班室)

    編輯部郵箱:casweb@cashq.ac.cn

  • © 1996 - 中國科學院 版權所有
    京ICP備05002857號-1
    京公網安備110402500047號
    網站標識碼bm48000002

    地址:北京市西城區三里河路52號 郵編:100864
    電話:86 10 68597114(總機)
       86 10 68597289(總值班室)
    編輯部郵箱:casweb@cashq.ac.cn