@techreport{oai:ipsj.ixsq.nii.ac.jp:00217249,
 author = {小池, 良吾 and 藤田, 昌宏},
 issue = {29},
 month = {Mar},
 note = {近年では論理回路の設計が大規模化し，設計を数学的に検証する形式的検証技術はより重要な技術になっている．その形式的検証技術の 1 つに順序回路の到達可能性を解析する Inductive Invariant がある．Inductive Invariant では特定のフリップフロップの集合に対して，順序回路が到達可能状態を計算することができる．Inductive Invariant では回路が持つすべてのフリップフロップからその一部を対象として計算を行うことで得られる状態は到達可能状態の上位集合となる．このようにすることで真の到達可能状態を計算するよりも計算量を抑えて解析を行うことが可能である．ここで計算の対象とするフリップフロップによって計算される到達可能状態の上位集合の大きさが変化する．本論文ではこのフリップフロップの選択方法を効率的に探索するアルゴリズムを提案し，またその計算量を削減する方法を提案した．提案手法はまずフリップフロップを選択する問題を QBF 問題として定式化し，それをインクリメンタルに解くことによって効率的な探索を可能にした．また Inductive Invariant の応用として計算された到達不可能な状態を利用して回路を最適化する方法を提案した．いずれの手法に関しても実験によって有効性を確認した．},
 title = {Inductive Invariantでの効率的フリップフロップ選択による形式的検証とその応用},
 year = {2022}
}