Differences

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

--- start [2026/06/22 07:15] – [オートマトン理論] kenji_saotome
+++ start [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年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 "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 95: / Line 95: @@
 自動形式検証のもう一つの代表的な手法として、演繹的検証（Deductive Verification）がある。
 演繹的検証では、プログラムとその仕様から論理的な制約を生成し、それらの制約を解くことによって、プログラムが仕様を満たすかどうかを判定する。
-//不動点論理//（Fixpoint Logics）は、最小不動点や最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。
+//不動点論理//（Fixpoint Logics）は、最小不動点および最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。
-基本的に、多くの意味論において、プログラム中のループの意味論をある作用素の最小不動点として表現できる。
+基本的な考え方として、多くの異なる意味論において、プログラムのループの意味論をある作用素の最小不動点として表現できる。したがって、プログラム全体の意味論を計算する問題は、本質的には最小不動点を計算する問題へと帰着される。
-そのため、プログラム全体の意味論を計算する問題は、本質的には不動点を計算する問題へと帰着される。
-解きたい問題に応じては、不動点論理の問題へ変換することができる。
-例えば、不動点論理の方程式の下界や上界を求める問題として帰着できる場合がある。
-こうした問題を自動化するための代表的な手法の一つが、テンプレートを使う事である。
-例えば、不動点の下界や上界を求めたい場合は、テンプレートを使うと、求める上界か下界が予め与えられた形状を持つと仮定する。
-例えば、「固定次数の多項式で表される」である事と仮定する。
-この仮定を導入すると、界が満たすべき条件は、そのテンプレートのパラメータに関する制約へと変換される。
-多項式テンプレートの場合であれば、多項式の係数に対する制約が得られる。
-その結果、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換される。
-==== SATとSMTソルバー ====
+解きたい問題によっては、不動点論理の方程式の下界や上界を求める問題などの不動点論理の問題として帰着できる場合がある。
+こうした問題を自動化するための代表的な手法の一つが、テンプレートの利用である。
+例えば不動点の下界や上界を求める場合、テンプレートを用いたアプローチでは、求める界が予め与えられた形状（例えば　固定次数の多項式）を持つと仮定する。
+これにより、界が満たすべき条件は、テンプレートのパラメータに関する制約（例えば　多項式の係数に関する制約）へと変換される。
+このように、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。
-演繹的検証によって生成さられる制約を解く方法はいくつか存在する。
+==== SATソルバーとSMTソルバー ====
-一つの方法は、定理証明ソフトウェア（proof assistants）を利用することである。
-定理証明ソフトウェアを用いると、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
+演繹的検証によって生成された制約を解く方法はいくつか存在する。
+一つの方法は、定理証明ソフトウェア（proof assistants）を利用する方法で、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。
-しかし、その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
+その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。
 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。
@@ Line 125: / Line 121: @@
 | 教授 | [[https://www.riec.tohoku.ac.jp/~unno/|海野 広志]] |
 | 助教 | [[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|門馬 琢磨]] |
@@ Line 156: / Line 152: @@
 研究室は[[https://www.riec.tohoku.ac.jp/ja/top/access/|東北大学電気通信研究所]]本館の五階にあります。
-教員達と研究員達はM518室とM519室にいます。
+教員と研究員はM518室とM519室、学生はM536室とM537室にいます。
-学生達はM536室とM537室にいます。
+また、輪読とセミナーにM522室を使用しています。
-M522室は輪読とセミナーに使います。
 ===== リンク =====