Differences

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

--- start [2026/06/22 07:31] – [不動点論理] 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 104: / Line 104: @@
 このように、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。
-==== SATとSMTソルバー ====
+==== SATソルバーとSMTソルバー ====
-演繹的検証によって生成さられる制約を解く方法はいくつか存在する。
+演繹的検証によって生成された制約を解く方法はいくつか存在する。
-一つの方法は、定理証明ソフトウェア（proof assistants）を利用することである。
+一つの方法は、定理証明ソフトウェア（proof assistants）を利用する方法で、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
-定理証明ソフトウェアを用いると、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。
-しかし、その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
+その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。
 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。
@@ Line 122: / 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 153: / Line 152: @@
 研究室は[[https://www.riec.tohoku.ac.jp/ja/top/access/|東北大学電気通信研究所]]本館の五階にあります。
-教員達と研究員達はM518室とM519室にいます。
+教員と研究員はM518室とM519室、学生はM536室とM537室にいます。
-学生達はM536室とM537室にいます。
+また、輪読とセミナーにM522室を使用しています。
-M522室は輪読とセミナーに使います。
 ===== リンク =====