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:49] – [形式検証] 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 69: Line 69:
 ==== 型理論 ==== ==== 型理論 ====
  
-プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）を利用する方法がある。+プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）の利用がある。
 その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。 その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。
 > Well-typed programs cannot go wrong. > Well-typed programs cannot go wrong.
Line 80: Line 80:
  
 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。
-モデル検査では、まず対象となるシステムを有限状態機械へ変換する。 +モデル検査では、まず対象となるシステムを有限状態機械(通常はオートマトン)へ変換する。ただしこの際、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 
-変換は、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 +同様に、仕様についても、受理言語が仕様によって許容される振る舞いを正確に表現するような有限状態機械へ変換する。 
-同様に、仕様についても有限状態機械へ変換し、その受理言語が仕様によって許容される振る舞いを正確に表現する。 +システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかの言語包含性をオートマトン理論に基づき自動的に検証する。
-システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかを判定すればよい。 +
-モデル検査では、この言語包含性をオートマトン理論などに基づく手法によって自動的に検証する。+
  
-この手法は、コントローラー合成（controller synthesis）などのプログラム合成にも応用できる。 +この手法は、コントローラー合成（controller synthesis）などのある種の合成問題の解決にも応用できる。 
-コントローラ合成では、例えばロボットのような制御対象システムが与えられ、そのシステムを仕様どおりに動作させるための制御プログラム（コントローラー）を自動生成することを目的とする。+コントローラ合成では、制御対象システム（例えばロボット）があるとき、そのシステムが仕様どおりに動作するための制御プログラム（コントローラー）を自動生成することを目的とする。
 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。
-例えば、現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 +例えば、システムの現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 
-この場合も、システムと仕様はそれぞれオートマトンへ変換される。 +この場合も、システムと仕様はそれぞれオートマトンへ変換されるが、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 
-しかし、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 +その代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを構築し、そのゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換するという古典的なアプローチが採用される。
-代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを生成する。 +
-このゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換することができる。+
  
 ==== 不動点論理 ==== ==== 不動点論理 ====
Line 99: 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 129: 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 160: 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.1782107385.txt.gz · Last modified: by kenji_saotome