現代社会において、人々は私生活や仕事において日常的にスマートフォンやコンピュータを用いており、普段意識されない交通・金融・医療・エネルギーといったコンピュータにより制御されているインフラは、極めて重要な役割を果たしている。したがって、コンピュータを制御するソフトウェアの信頼性を確保し、その効率性を向上させることは、社会の安定と円滑な機能の維持にとって重要な課題である。本研究室では、形式論理やプログラム理論といった基礎理論に基づいた高信頼かつ高効率なソフトウェアを構成する技術について研究を行っている。

• 2026年6月. The paper “A Hierarchy of Supermartingales for ω-Regular Verification” by Professor Hiroshi Unno et al. was presented at PLDI 2026.
• 2026年6月. The paper “Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification” by Professor Hiroshi Unno et al. was presented at PLDI 2026.
• 2026年5月. Professor Hiroshi Unno gave a keynote talk at ISMVL 2026.
• 2026年4月. We participated in CHC-COMP 2026 with PCSat and MuCyc, two CHC solvers developed in our laboratory.
• 2026年4月. The paper “A Category-Theoretic Framework for Dependent Effect Systems” by Professor Hiroshi Unno et al. was presented at ESOP 2026.
• 2026年3月. Takuma Monma and Kazuki Uehara have presented posters about their research at PPL 2026.
• 2025年11月. The paper “AP-observation Automata for Abstraction-based Verification of Continuous-time Systems” by Assistant Professor Clovis Eberhart et al. was presented at ICTAC 2025.
• 2025年10月. The paper “On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs” by Professor Hiroshi Unno et al. was presented at OOPSLA 2025.
• 2025年10月. Takuma Monma, Kazuki Uehara, and Assistant Professor Clovis Eberhart presented a demonstration at the RIEC Open House 2025.
• 2025年9月. MuVal, a verification tool developed in our laboratory, won the C category at Termination Competition 2024.
• 2025年6月. The paper “Thrust: A Prophecy-based Refinement Type System for Rust” by Professor Hiroshi Unno et al. was presented at PLDI 2025.
• 2025年5月. Professor Hiroshi Unno gave an invited lecture at EPIT 2025.
• 2025年5月. Professor Hiroshi Unno gave an invited talk at a "CHoCoLa" meeting.
• 2025年5月. Assistant Professor Clovis Eberhart has joined our laboratory.
• 2025年4月. We participated in CHC-COMP 2025 with PCSat and MuCyc, two CHC solvers developed in our laboratory.
• 2025年4月. Professor Hiroshi Unno's project, “Foundations and Applications of Program Verification Techniques,” has been selected for funding under the 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 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 POPL 2025.
• 2025年1月. The paper “A Primal-Dual Perspective on Program Verification Algorithms” by Professor Hiroshi Unno et al. was presented at 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 POPL 2025.
• 2024年10月. The paper “Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification” by Professor Hiroshi Unno et al. was presented at OOPSLA 2024.
• 2024年9月. The paper “Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System” by Professor Hiroshi Unno et al. was presented at ICFP 2024.
• 2024年7月. MuVal, a verification tool developed in our laboratory, won the Integer Transition Systems category at Termination Competition 2024.
• 2024年6月. The paper “Inductive Approach to Spacer” by Professor Hiroshi Unno et al. was presented at PLDI 2024.
• 2024年4月. Professor Hiroshi Unno joined Tohoku University and started the Software Construction Laboratory.

ソフトウェアとハードウェアの不具合は

• 経済的損失（Ethereum DAOへの攻撃、 $55M盗難）
• 社会的損失（KDDI通信障害が二日間以上続く, ハートブリードというソフトウェア・バグによってOpenSSLの暗号化メッセージが復号可能になる）および,
• 人的損失（Therac-25放射線治療器具の誤動作による医療事故）

を招くことがある。

バグのないコードを書くための最も一般的な方法は、モジュール化されたコードの記述、明確なドキュメントの作成、徹底したコードレビューの実施、あるいは十分なテストスイートの整備など、バグを作り込む可能性を低減する一連の「ベストプラクティス」に従うことである。 しかし、これらの手法はバグが発生する可能性を減らすに過ぎず、未発見のバグが存在しないことを保証することはできない。 形式検証（Formal Verification）の目的は、

• システム（例えば、コンピュータプログラムや物理対象のモデル）および、
• 形式仕様（すなわち、望ましい振る舞いの曖昧さのない記述）

が与えられたときに、システムが仕様に従って振る舞うか自動的に判定することである。 形式検証では、対象となるシステムや仕様の種類に応じて、形式論理、型システム、プログラミング言語の意味論、オートマトン理論などの理論を活用する。

形式検証によって、すでに作成されたソフトウェアにバグが存在しないことを保証できる。 しかし、ソフトウェアにバグが含まれていた場合、検証手法の大半はそのバグがどこにあるのか、あるいはどのように修正すればよいのかを示してくれない。 こうした問題を扱う分野は、バグ自動修正（Automated Program Repair）とバグ局所化（Fault Localization）と呼ばれる。 一方で、ソフトウェアにバグが存在しないことを保証する別の方法として、そもそもバグが入り込まないような形でソフトウェアを生成するという考え方がある。 これは「Correct-by-Design」あるいは「Correct-by-Construction」と呼ばれることがある。 この考え方を扱うのがプログラム合成（Program Synthesis）の分野である。 プログラム合成は形式検証と密接に関連しており、多くの場合、同じ理論や技術を利用するが、その目的はやや異なる。 プログラム合成では、形式検証と違って、形式仕様のみが与えられ、システムは与えられない。 このときの目標は、与えられた仕様を満たすシステムを自動的に生成することである。

プログラムにバグが存在しないことを証明する方法の一つとして、型システム（type systems）の利用がある。 その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。

Well-typed programs cannot go wrong.

「適切に型付けされたプログラムは誤動作しない。」 MLなどの伝統的な型システムにおいて、この主張は主に二つの定理によって形式化される。 第一に、進行定理（progress theorem）は、型付けされたプログラムが実行途中で行き詰まることはないことを述べる。 第二に、保存定理（preservation theorem）は、型付けされたプログラムを評価した結果も同じ型を持つことを述べる。

自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。 モデル検査では、まず対象となるシステムを有限状態機械(通常はオートマトン)へ変換する。ただしこの際、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 同様に、仕様についても、受理言語が仕様によって許容される振る舞いを正確に表現するような有限状態機械へ変換する。 システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかの言語包含性をオートマトン理論に基づき自動的に検証する。

この手法は、コントローラー合成（controller synthesis）などのある種の合成問題の解決にも応用できる。 コントローラ合成では、制御対象システム（例えばロボット）があるとき、そのシステムが仕様どおりに動作するための制御プログラム（コントローラー）を自動生成することを目的とする。 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。 例えば、システムの現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 この場合も、システムと仕様はそれぞれオートマトンへ変換されるが、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 その代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを構築し、そのゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換するという古典的なアプローチが採用される。

自動形式検証のもう一つの代表的な手法として、演繹的検証（Deductive Verification）がある。 演繹的検証では、プログラムとその仕様から論理的な制約を生成し、それらの制約を解くことによって、プログラムが仕様を満たすかどうかを判定する。 不動点論理（Fixpoint Logics）は、最小不動点および最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。 基本的な考え方として、多くの異なる意味論において、プログラムのループの意味論をある作用素の最小不動点として表現できる。したがって、プログラム全体の意味論を計算する問題は、本質的には最小不動点を計算する問題へと帰着される。

解きたい問題によっては、不動点論理の方程式の下界や上界を求める問題などの不動点論理の問題として帰着できる場合がある。 こうした問題を自動化するための代表的な手法の一つが、テンプレートの利用である。 例えば不動点の下界や上界を求める場合、テンプレートを用いたアプローチでは、求める界が予め与えられた形状（例えば　固定次数の多項式）を持つと仮定する。 これにより、界が満たすべき条件は、テンプレートのパラメータに関する制約（例えば　多項式の係数に関する制約）へと変換される。 このように、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。

演繹的検証によって生成された制約を解く方法はいくつか存在する。 一つの方法は、定理証明ソフトウェア（proof assistants）を利用する方法で、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。 その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。 これらは、特定の問題クラスを効率的に解くために設計・最適化されたソフトウェアであり、形式検証やプログラム解析において広く利用されている。

研究室は東北大学電気通信研究所本館の五階にあります。 教員と研究員はM518室とM519室、学生はM536室とM537室にいます。 また、輪読とセミナーにM522室を使用しています。

• 東北大学
• 東北大学電気通信研究所