sclab

User Tools

Site Tools

Trace: • start
start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
start [2026/06/22 05:43] – [形式検証] kenji_saotomestart [2026/06/25 12:39] (current) – hiroshi_unno
Line 24: Line 24:
  * **2025年4月**. Professor **Hiroshi Unno**'s project, "Foundations and Applications of Program Verification Techniques," has been selected for funding under the [[https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-25H00446/|KAKENHI Grant-in-Aid for Scientific Research (S)]].  * **2025年4月**. Professor **Hiroshi Unno**'s project, "Foundations and Applications of Program Verification Techniques," has been selected for funding under the [[https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-25H00446/|KAKENHI Grant-in-Aid for Scientific Research (S)]].
  * **2025年2月**. The paper "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking" by Professor **Hiroshi Unno** et al. was presented at [[https://aaai.org/conference/aaai/aaai-25/|AAAI 2025]].  * **2025年2月**. The paper "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking" by Professor **Hiroshi Unno** et al. was presented at [[https://aaai.org/conference/aaai/aaai-25/|AAAI 2025]].
- * **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor Hiroshi Unno et al. received a **Distinguished Paper Award** at [[https://popl25.sigplan.org/|POPL 2025]].+ * **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor **Hiroshi Unno** et al. received a **Distinguished Paper Award** at [[https://popl25.sigplan.org/|POPL 2025]].
  * **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].  * **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].
  * **2025年1月**. The paper "Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].  * **2025年1月**. The paper "Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].
Line 43: Line 43:
 ソフトウェアとハードウェアの不具合は ソフトウェアとハードウェアの不具合は
  * 経済的損失（[[https://ja.wikipedia.org/wiki/イーサリアムクラシック|Ethereum DAOへの攻撃、 $55M盗難]]）  * 経済的損失（[[https://ja.wikipedia.org/wiki/イーサリアムクラシック|Ethereum DAOへの攻撃、 $55M盗難]]）
- * 社会的損失（[[https://www.kddi.com/important-news/20220729_01/|KDDI通信障害が二日間以上続く]], および[[https://ja.wikipedia.org/wiki/%E3%83%8F%E3%83%BC%E3%83%88%E3%83%96%E3%83%AA%E3%83%BC%E3%83%89|ハートブリードというソフトウェア・バグによってOpenSSLの暗号化メッセージが復号可能になる]]）+ * 社会的損失（[[https://www.kddi.com/important-news/20220729_01/|KDDI通信障害が二日間以上続く]], [[https://ja.wikipedia.org/wiki/%E3%83%8F%E3%83%BC%E3%83%88%E3%83%96%E3%83%AA%E3%83%BC%E3%83%89|ハートブリードというソフトウェア・バグによってOpenSSLの暗号化メッセージが復号可能になる]]）および,
  * 人的損失（[[https://ja.wikipedia.org/wiki/%E3%82%BB%E3%83%A9%E3%83%83%E3%82%AF25|Therac-25放射線治療器具の誤動作による医療事故]]）  * 人的損失（[[https://ja.wikipedia.org/wiki/%E3%82%BB%E3%83%A9%E3%83%83%E3%82%AF25|Therac-25放射線治療器具の誤動作による医療事故]]）
-を招くことがあります。+を招くことがある。
  
-バグのないコードを書くための最も一般的な方法は、バグを作り込む可能性を低減する「ベストプラクティス」に従うことである。 +バグのないコードを書くための最も一般的な方法は、モジュール化されたコードの記述、明確なドキュメントの作成、徹底したコードレビューの実施、あるいは十分なテストスイートの整備など、バグを作り込む可能性を低減する一連の「ベストプラクティス」に従うことである。 
-それはたとえばモジュール化されたコードを書くこと、明確なドキュメントを作成すること、徹底したコードレビューを実施すること、あるいは十分なテストスイートを整備するといった。 +しかし、これらの手法はバグが発生する可能性を減らすに過ぎず、未発見のバグが存在しないことを保証することはできない。
-しかし、これらの手法はバグが発生する可能性を減らすことはできても、未発見のバグが存在しないことを保証することはできない。+
 形式検証（Formal Verification）の目的は、 形式検証（Formal Verification）の目的は、
- * システム（例えば、コンピュータプログラムや物理対象のモデル） + * システム（例えば、コンピュータプログラムや物理対象のモデル）および、 
- * および形式仕様（すなわち、望ましい振る舞いを曖昧さなく記述したもの） + * 形式仕様（すなわち、望ましい振る舞いの曖昧さのない記述） 
-が与えられたときに、そのシステムが仕様に従って振る舞うかどうかを自動的に判定することである。 +が与えられたときに、システムが仕様に従って振る舞うか自動的に判定することである。 
-形式検証では、対象となるシステムと仕様の種類に応じて、形式論理、型システム、プログラミング言語の意味論、オートマトン理論などの理論を活用する。+形式検証では、対象となるシステムや仕様の種類に応じて、形式論理、型システム、プログラミング言語の意味論、オートマトン理論などの理論を活用する。
  
 ==== プログラム合成 ==== ==== プログラム合成 ====
Line 70: Line 69:
 ==== 型理論 ==== ==== 型理論 ====
  
-プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）を利用する方法がある。+プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）の利用がある。
 その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。 その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。
 > Well-typed programs cannot go wrong. > Well-typed programs cannot go wrong.
Line 81: Line 80:
  
 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。
-モデル検査では、まず対象となるシステムを有限状態機械へ変換する。 +モデル検査では、まず対象となるシステムを有限状態機械(通常はオートマトン)へ変換する。ただしこの際、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 
-変換は、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 +同様に、仕様についても、受理言語が仕様によって許容される振る舞いを正確に表現するような有限状態機械へ変換する。 
-同様に、仕様についても有限状態機械へ変換し、その受理言語が仕様によって許容される振る舞いを正確に表現する。 +システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかの言語包含性をオートマトン理論に基づき自動的に検証する。
-システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかを判定すればよい。 +
-モデル検査では、この言語包含性をオートマトン理論などに基づく手法によって自動的に検証する。+
  
-この手法は、コントローラー合成（controller synthesis）などのプログラム合成にも応用できる。 +この手法は、コントローラー合成（controller synthesis）などのある種の合成問題の解決にも応用できる。 
-コントローラ合成では、例えばロボットのような制御対象システムが与えられ、そのシステムを仕様どおりに動作させるための制御プログラム（コントローラー）を自動生成することを目的とする。+コントローラ合成では、制御対象システム（例えばロボット）があるとき、そのシステムが仕様どおりに動作するための制御プログラム（コントローラー）を自動生成することを目的とする。
 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。
-例えば、現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 +例えば、システムの現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 
-この場合も、システムと仕様はそれぞれオートマトンへ変換される。 +この場合も、システムと仕様はそれぞれオートマトンへ変換されるが、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 
-しかし、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 +その代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを構築し、そのゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換するという古典的なアプローチが採用される。
-代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを生成する。 +
-このゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換することができる。+
  
 ==== 不動点論理 ==== ==== 不動点論理 ====
Line 100: Line 95:
 自動形式検証のもう一つの代表的な手法として、演繹的検証（Deductive Verification）がある。 自動形式検証のもう一つの代表的な手法として、演繹的検証（Deductive Verification）がある。
 演繹的検証では、プログラムとその仕様から論理的な制約を生成し、それらの制約を解くことによって、プログラムが仕様を満たすかどうかを判定する。 演繹的検証では、プログラムとその仕様から論理的な制約を生成し、それらの制約を解くことによって、プログラムが仕様を満たすかどうかを判定する。
-//不動点論理//（Fixpoint Logics）は、最小不動点や最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。 +//不動点論理//（Fixpoint Logics）は、最小不動点および最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。 
-基本的に、多くの意味論において、プログラム中のループの意味論をある作用素の最小不動点として表現できる。 +基本的な考え方として、多くの異なる意味論において、プログラムのループの意味論をある作用素の最小不動点として表現できる。したがって、プログラム全体の意味論を計算する問題は、本質的には最小不動点を計算する問題へと帰着される。
-そのため、プログラム全体の意味論を計算する問題は、本質的には不動点を計算する問題へと帰着される。 +
-解きたい問題に応じては、不動点論理の問題へ変換することができる。 +
-例えば、不動点論理の方程式の下界や上界を求める問題として帰着できる場合がある。 +
-こうした問題を自動化するための代表的な手法の一つが、テンプレートを使う事である。 +
-例えば、不動点の下界や上界を求めたい場合は、テンプレートを使うと、求める上界か下界が予め与えられた形状を持つと仮定する。 +
-例えば、「固定次数の多項式で表される」である事と仮定する。 +
-この仮定を導入すると、界が満たすべき条件は、そのテンプレートのパラメータに関する制約へと変換される。 +
-多項式テンプレートの場合であれば、多項式の係数に対する制約が得られる。 +
-その結果、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換される。+
  
-==== SATとSMTソルバー ====+解きたい問題によっては、不動点論理の方程式の下界や上界を求める問題などの不動点論理の問題として帰着できる場合がある。 
 +こうした問題を自動化するための代表的な手法の一つが、テンプレートの利用である。 
 +例えば不動点の下界や上界を求める場合、テンプレートを用いたアプローチでは、求める界が予め与えられた形状（例えば　固定次数の多項式）を持つと仮定する。 
 +これにより、界が満たすべき条件は、テンプレートのパラメータに関する制約（例えば　多項式の係数に関する制約）へと変換される。 
 +このように、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。
  
-演繹的検証によって生成さられる制約を解く方法はいくつか存在する。 +==== SATソルバーとSMTソルバー ==== 
-一つの方法は、定理証明ソフトウェア（proof assistants）を利用することである。 + 
-定理証明ソフトウェアを用いると、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。+演繹的検証によって生成された制約を解く方法はいくつか存在する。 
 +一つの方法は、定理証明ソフトウェア（proof assistants）を利用する方法で、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。
-しかし、その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。+その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。
 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。
Line 130: Line 121:
 | 教授 | [[https://www.riec.tohoku.ac.jp/~unno/|海野 広志]] | | 教授 | [[https://www.riec.tohoku.ac.jp/~unno/|海野 広志]] |
 | 助教 | [[https://www.riec.tohoku.ac.jp/~eberhart/|Eberhart Clovis]] | | 助教 | [[https://www.riec.tohoku.ac.jp/~eberhart/|Eberhart Clovis]] |
-| 博士研究員 | [[https://researchmap.jp/k_saotome?lang=en|早乙女 献自]] |+| 特任研究員 | [[https://researchmap.jp/k_saotome?lang=ja|早乙女 献自]] |
 | 秘書 | 寒河江 香子 | | 秘書 | 寒河江 香子 |
 | 修士課程  | [[takuma_monma|門馬 琢磨]] | | 修士課程  | [[takuma_monma|門馬 琢磨]] |
Line 161: Line 152:
  
 研究室は[[https://www.riec.tohoku.ac.jp/ja/top/access/|東北大学電気通信研究所]]本館の五階にあります。 研究室は[[https://www.riec.tohoku.ac.jp/ja/top/access/|東北大学電気通信研究所]]本館の五階にあります。
-教員達と研究員達はM518室とM519室にいます。 +教員と研究員はM518室とM519室、学生はM536室とM537室にいます。 
-学生達はM536室とM537室にいます。 +また、輪読とセミナーにM522室を使用しています。
-M522室は輪読とセミナーに使います。+
  
 ===== リンク ===== ===== リンク =====
start.1782107000.txt.gz · Last modified: by kenji_saotome