核心概念
帰納的検証において、無限モデルを見つける新しい手法を提案する。
摘要
第一階述語論理と量化子はプログラムやシステムの帰納的検証で広く使用されている。
既存のツールは有限モデルを見つけることができるが、無限モデルを見つけられない場合がある。
記事では、無限モデルを表現するための象徴的構造が導入され、その効率的なチェック方法が示されている。
新しい決定可能な断片「Ordered Self Cycle (OSC)」は多数ソートEPRの拡張であり、満足性問題が決定可能であることが示されている。
FEST(Find and Evaluate Symbolic structures via Templates)というツールは21個の例題で成功裏に適用され、既存のソルバーでは解決できなかった問題に対して無限カウンターモデルを素早く見つけた。
統計資料
量化子は自動ソルバーにとって難しい課題を提供する。
現在のソルバーは無限モデルを見つけられない場合がある。
引述
"Quantifiers provide expressivity, but pose a significant challenge for automated verification."
"Our approach consists of three parts: symbolic structures, model finding procedure, and a new decidable fragment of first-order logic."