| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| start [2026/06/22 05:49] – [形式検証] kenji_saotome | start [2026/09/27 07:38] (current) – external edit 127.0.0.1 |
|---|
| ===== 最新のニュース ===== | ===== 最新のニュース ===== |
| |
| * **2026年6月**. The paper "A Hierarchy of Supermartingales for ω-Regular Verification" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi26.sigplan.org/|PLDI 2026]]. | * **2026年9月**. **海野 広志**教授が主たる共同研究者を務める研究課題「ビスポーク型トランザクション処理エンジンの構築」（研究開発代表者：川島 英之教授）が、[[https://www.jst.go.jp/kisoken/cronos/index.html|JST CRONOS]] に採択されました。 |
| * **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 [[https://pldi26.sigplan.org/|PLDI 2026]]. | * **2026年9月**. **海野 広志**教授が [[https://ses.sigse.jp/2026/|SES 2026]] において**卓越研究賞**を受賞しました。 |
| * **2026年5月**. Professor **Hiroshi Unno** gave a keynote talk at [[https://mvl.jpn.org/ISMVL2026/|ISMVL 2026]]. | * **2026年8月**. **海野 広志**教授らによる論文 "Automated Safety Verification of Posterior Distributions of Probabilistic Programs" が [[https://2026.ijcai.org/|IJCAI 2026]] で発表されました。 |
| * **2026年4月**. We participated in [[https://chc-comp.github.io/chc-comp-2026/tables/index.html|CHC-COMP 2026]] with **PCSat** and **MuCyc**, two CHC solvers developed in our laboratory. | * **2026年7月**. [[https://www.online-opencampus.tnc.tohoku.ac.jp/index.html|東北大学オープンキャンパス2026]]にて、**岡田 渉汰**さん、**渡辺 大也**さん、**植原 一希**さん、**Clovis Eberhart** 助教がポスター展示および本研究室で開発している検証ツール **Athena** および **Thrust** のデモ展示を行いました。 |
| * **2026年4月**. The paper "A Category-Theoretic Framework for Dependent Effect Systems" by Professor **Hiroshi Unno** et al. was presented at [[https://etaps.org/2026/conferences/esop/|ESOP 2026]]. | * **2026年7月**. **海野 広志**教授らによる論文 "Lagrangian-Based Duality for Quantified SMT Algorithms" が [[https://conferences.i-cav.org/2026/|CAV 2026]] で発表されました。 |
| * **2026年3月**. **Takuma Monma** and **Kazuki Uehara** have presented posters about their research at [[https://jssst-ppl.org/workshop/2026/|PPL 2026]]. | * **2026年7月**. 本研究室で開発している検証ツール **MuVal** で [[https://termcomp.github.io/Y2026/|Termination Competition 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 [[https://ictac2025.digital-hub.sh/|ICTAC 2025]]. | * **2026年7月**. **門馬 琢磨**さんが、**Clovis Eberhart** 助教および **海野 広志**教授との共同研究 "Probabilistic Loop Acceleration via a Quantitative Fixpoint Logic" を [[https://veriprop.github.io/2026/|VeriProP 2026]] で発表しました。 |
| * **2025年10月**. The paper "On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://2025.splashcon.org/|OOPSLA 2025]]. | * **2026年7月**. **海野 広志**教授らによる論文 "Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition" が [[https://satisfiability.org/SAT26/|SAT 2026]] で発表されました。 |
| * **2025年10月**. **Takuma Monma**, **Kazuki Uehara**, and Assistant Professor **Clovis Eberhart** presented a demonstration at the [[https://www.riec.tohoku.ac.jp/koukai/koukai2025/|RIEC Open House 2025]]. | * **2026年6月**. **海野 広志**教授らによる論文 "A Hierarchy of Supermartingales for ω-Regular Verification" が [[https://pldi26.sigplan.org/|PLDI 2026]] で発表されました。 |
| * **2025年9月**. **MuVal**, a verification tool developed in our laboratory, won the C category at [[https://termcomp.github.io/Y2025/|Termination Competition 2024]]. | * **2026年6月**. **海野 広志**教授らによる論文 "Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification" が [[https://pldi26.sigplan.org/|PLDI 2026]] で発表されました。 |
| * **2025年6月**. The paper "Thrust: A Prophecy-based Refinement Type System for Rust" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi25.sigplan.org/|PLDI 2025]]. | * **2026年6月**. **海野 広志**教授らによる論文 "Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs" が [[https://pldi26.sigplan.org/home/ARRAY-2026|ARRAY 2026]] で発表されました。 |
| * **2025年5月**. Professor **Hiroshi Unno** gave an invited lecture at [[https://epit2025.sciencesconf.org/|EPIT 2025]]. | * **2026年5月**. **海野 広志**教授が [[https://mvl.jpn.org/ISMVL2026/|ISMVL 2026]] で基調講演を行いました。 |
| * **2025年5月**. Professor **Hiroshi Unno** gave an invited talk at a [[https://chocola.ens-lyon.fr/events/meeting-2025-05-15/|"CHoCoLa" meeting]]. | * **2026年4月**. 本研究室で開発している2つのCHCソルバー **PCSat** と **MuCyc** で [[https://chc-comp.github.io/chc-comp-2026/tables/index.html|CHC-COMP 2026]] に参加しました。 |
| * **2025年5月**. Assistant Professor **Clovis Eberhart** has joined our laboratory. | * **2026年4月**. **海野 広志**教授らによる論文 "A Category-Theoretic Framework for Dependent Effect Systems" が [[https://etaps.org/2026/conferences/esop/|ESOP 2026]] で発表されました。 |
| * **2025年4月**. We participated in [[https://chc-comp.github.io/2025/|CHC-COMP 2025]] with **PCSat** and **MuCyc**, two CHC solvers developed in our laboratory. | * **2026年4月**. **早乙女 献自**特任研究員が本研究室に着任しました。 |
| * **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)]]. | * **2026年3月**. **門馬 琢磨**さんが「量的不動点論理を用いた確率的プログラム検証のためのLoop Acceleration」、**植原 一希**さんが「Rustイテレータのためのリファインメント型推論」を [[https://jssst-ppl.org/workshop/2026/|PPL 2026]] でポスター発表しました。 |
| * **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年11月**. **Clovis Eberhart** 助教らによる論文 "AP-observation Automata for Abstraction-based Verification of Continuous-time Systems" が [[https://ictac2025.digital-hub.sh/|ICTAC 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年10月**. **海野 広志**教授らによる論文 "On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs" が [[https://2025.splashcon.org/|OOPSLA 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年10月**. **門馬 琢磨**さん、**植原 一希**さん、**Clovis Eberhart** 助教が [[https://www.riec.tohoku.ac.jp/koukai/koukai2025/|電気通信研究所一般公開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年9月**. 本研究室で開発している検証ツール **MuVal** が、[[https://termcomp.github.io/Y2025/|Termination Competition 2025]] の C 部門で優勝しました。 |
| * **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 [[https://2024.splashcon.org/|OOPSLA 2024]]. | * **2025年6月**. **海野 広志**教授らによる論文 "Thrust: A Prophecy-based Refinement Type System for Rust" が [[https://pldi25.sigplan.org/|PLDI 2025]] で発表されました。 |
| * **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 [[https://icfp24.sigplan.org/|ICFP 2024]]. | * **2025年5月**. **海野 広志**教授が [[https://epit2025.sciencesconf.org/|EPIT 2025]] で招待講義を行いました。 |
| * **2024年7月**. **MuVal**, a verification tool developed in our laboratory, won the Integer Transition Systems category at [[https://termcomp.github.io/Y2024/|Termination Competition 2024]]. | * **2025年5月**. **海野 広志**教授が [[https://chocola.ens-lyon.fr/events/meeting-2025-05-15/|CHoCoLa ミーティング]] で招待講演を行いました。 |
| * **2024年6月**. The paper "Inductive Approach to Spacer" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi24.sigplan.org/|PLDI 2024]]. | * **2025年5月**. **Clovis Eberhart** 助教が本研究室に着任しました。 |
| * **2024年4月**. Professor **Hiroshi Unno** joined Tohoku University and started the Software Construction Laboratory. | * **2025年4月**. 本研究室で開発している2つのCHCソルバー **PCSat** と **MuCyc** で [[https://chc-comp.github.io/2025/|CHC-COMP 2025]] に参加しました。 |
| | * **2025年4月**. **海野 広志**教授の研究課題「プログラム検証技術の基礎付けと応用」が、[[https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-25K24739/|科学研究費助成事業 基盤研究(S)]] に採択されました。 |
| | * **2025年2月**. **海野 広志**教授らによる論文 "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking" が [[https://aaai.org/conference/aaai/aaai-25/|AAAI 2025]] で発表されました。 |
| | * **2025年1月**. **海野 広志**教授らによる論文 "A Primal-Dual Perspective on Program Verification Algorithms" が [[https://popl25.sigplan.org/|POPL 2025]] で **Distinguished Paper Award** を受賞しました。 |
| | * **2025年1月**. **海野 広志**教授らによる論文 "A Primal-Dual Perspective on Program Verification Algorithms" が [[https://popl25.sigplan.org/|POPL 2025]] で発表されました。 |
| | * **2025年1月**. **海野 広志**教授らによる論文 "Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs" が [[https://popl25.sigplan.org/|POPL 2025]] で発表されました。 |
| | * **2024年10月**. **海野 広志**教授らによる論文 "Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification" が [[https://2024.splashcon.org/|OOPSLA 2024]] で発表されました。 |
| | * **2024年9月**. **海野 広志**教授らによる論文 "Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System" が [[https://icfp24.sigplan.org/|ICFP 2024]] で発表されました。 |
| | * **2024年7月**. 本研究室で開発している検証ツール **MuVal** が、[[https://termcomp.github.io/Y2024/|Termination Competition 2024]] の Integer Transition Systems 部門で優勝しました。 |
| | * **2024年6月**. **海野 広志**教授らによる論文 "Inductive Approach to Spacer" が [[https://pldi24.sigplan.org/|PLDI 2024]] で発表されました。 |
| | * **2024年4月**. **海野 広志**教授が東北大学に着任し、ソフトウェア構成研究室を設立しました。 |
| |
| ===== 研究室生活 ===== | ===== 研究室生活 ===== |
| ==== 型理論 ==== | ==== 型理論 ==== |
| |
| プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）を利用する方法がある。 | プログラムにバグが存在しないことを証明する方法の一つとして、//型システム//（type systems）の利用がある。 |
| その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。 | その基本的な考え方は、Robin Milnerの有名な次の言葉に端的に表されている。 |
| > Well-typed programs cannot go wrong. | > Well-typed programs cannot go wrong. |
| |
| 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。 | 自動形式検証の一般的な手法の一つに、モデル検査（Model Checking）がある。 |
| モデル検査では、まず対象となるシステムを有限状態機械へ変換する。 | モデル検査では、まず対象となるシステムを有限状態機械(通常はオートマトン)へ変換する。ただしこの際、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 |
| 変換は、有限状態機械の受理言語がシステムの取り得る振る舞いを正確に表現するようにする。 | 同様に、仕様についても、受理言語が仕様によって許容される振る舞いを正確に表現するような有限状態機械へ変換する。 |
| 同様に、仕様についても有限状態機械へ変換し、その受理言語が仕様によって許容される振る舞いを正確に表現する。 | システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかの言語包含性をオートマトン理論に基づき自動的に検証する。 |
| システムのすべての振る舞いが仕様によって許容されることを確認するためには、システムを表す有限状態機械の言語が仕様を表す有限状態機械の言語に含まれてるかどうかを判定すればよい。 | |
| モデル検査では、この言語包含性をオートマトン理論などに基づく手法によって自動的に検証する。 | |
| |
| この手法は、コントローラー合成（controller synthesis）などのプログラム合成にも応用できる。 | この手法は、コントローラー合成（controller synthesis）などのある種の合成問題の解決にも応用できる。 |
| コントローラ合成では、例えばロボットのような制御対象システムが与えられ、そのシステムを仕様どおりに動作させるための制御プログラム（コントローラー）を自動生成することを目的とする。 | コントローラ合成では、制御対象システム（例えばロボット）があるとき、そのシステムが仕様どおりに動作するための制御プログラム（コントローラー）を自動生成することを目的とする。 |
| 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。 | 仕様の種類によっては、合成されるコントローラの形式を単純なものに制限できる。 |
| 例えば、現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 | 例えば、システムの現在の状態のみに基づいて制御入力を決定するメモリレスコントローラーがその一例である。 |
| この場合も、システムと仕様はそれぞれオートマトンへ変換される。 | この場合も、システムと仕様はそれぞれオートマトンへ変換されるが、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 |
| しかし、形式検証の場合と違って、ここで関心があるのは言語包含性ではない。 | その代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを構築し、そのゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換するという古典的なアプローチが採用される。 |
| 代わりに、システムと仕様を表すオートマトンの積を構成し、そこから数学的ゲームを生成する。 | |
| このゲームにおける必勝戦略を求めることで、その戦略を仕様を満たすコントローラーへと変換することができる。 | |
| |
| ==== 不動点論理 ==== | ==== 不動点論理 ==== |
| 自動形式検証のもう一つの代表的な手法として、演繹的検証（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）ソルバーである。 |
| | 教授 | [[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|門馬 琢磨]] | |
| |
| ^ DL ^ 論文タイトル ^ 著者名 ^ 雑誌・会議名 ^ | ^ DL ^ 論文タイトル ^ 著者名 ^ 雑誌・会議名 ^ |
| | | Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition | Jung-Cheng Lin, Chia-Hsuan Su, Jie-Hong R. Jiang, and Hiroshi Unno | [[https://satisfiability.org/SAT26/|International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) (to appear)]] | | | [[https://doi.org/10.24963/ijcai.2026/91|doi]] | Automated Safety Verification of Posterior Distributions of Probabilistic Programs | Kazuki Watanabe and Hiroshi Unno | [[https://2026.ijcai.org/|International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2026)]] | |
| | | Automated Safety Verification of Posterior Distributions of Probabilistic Programs | Kazuki Watanabe and Hiroshi Unno | [[https://2026.ijcai.org/|International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2026) (to appear)]] | | | [[https://doi.org/10.1007/978-3-032-32526-6_4|doi]] | Lagrangian-Based Duality for Quantified SMT Algorithms | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham | [[https://conferences.i-cav.org/2026/|International Conference on Computer Aided Verification (CAV 2026)]] | |
| | | Lagrangian-Based Duality for Quantified SMT Algorithms | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham | [[https://conferences.i-cav.org/2026/|International Conference on Computer Aided Verification (CAV 2026) (to appear)]] | | | [[https://doi.org/10.4230/LIPIcs.SAT.2026.24|doi]] | Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition | Jung-Cheng Lin, Chia-Hsuan Su, Jie-Hong R. Jiang, and Hiroshi Unno | [[https://satisfiability.org/SAT26/|International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)]] | |
| | | Sound Termination and Non-Termination Analysis of C Programs with Bit-Precise Bounded Semantics and Advanced Constructs | Negar Fathi, Hiroshi Unno, Tachio Terauchi, and Rahul Purandare | [[https://conf.researchr.org/home/fse-2026|International Conference on the Foundations of Software Engineering (FSE 2026) (to appear)]] | | | [[https://doi.org/10.1145/3808205|doi]] | Sound Termination and Non-Termination Analysis of C Programs with Bit-Precise Bounded Semantics and Advanced Constructs | Negar Fathi, Hiroshi Unno, Tachio Terauchi, and Rahul Purandare | [[https://conf.researchr.org/home/fse-2026|International Conference on the Foundations of Software Engineering (FSE 2026)]] | |
| | [[https://doi.org/10.1145/3808257|doi]] [[https://arxiv.org/abs/2512.00270|arXiv]] | A Hierarchy of Supermartingales for ω-Regular Verification | Satoshi Kura and Hiroshi Unno | [[https://pldi26.sigplan.org/|ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026)]] | | | [[https://doi.org/10.1145/3808257|doi]] [[https://arxiv.org/abs/2512.00270|arXiv]] | A Hierarchy of Supermartingales for ω-Regular Verification | Satoshi Kura and Hiroshi Unno | [[https://pldi26.sigplan.org/|ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026)]] | |
| | [[https://doi.org/10.1145/3808348|doi]] [[https://arxiv.org/abs/2504.04132|arXiv]] | Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification | Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada | [[https://pldi26.sigplan.org/|ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026)]] | | | [[https://doi.org/10.1145/3808348|doi]] [[https://arxiv.org/abs/2504.04132|arXiv]] | Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification | Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada | [[https://pldi26.sigplan.org/|ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026)]] | |
| |
| 研究室は[[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室は輪読とセミナーに使います。 | |
| |
| ===== リンク ===== | ===== リンク ===== |
