| Next revision | Previous revision |
| jp:start [2026/06/23 09:21] – created admin | jp:start [2026/09/27 07:38] (current) – [最新のニュース] hiroshi_unno |
|---|
| [[https://www.tohoku.ac.jp/japanese/|東北大学]] >> [[https://www.riec.tohoku.ac.jp/ja/|東北大学電気通信研究所]] >> ソフトウェア構成研究室 | [[https://www.tohoku.ac.jp/japanese/|東北大学]] >> [[https://www.riec.tohoku.ac.jp/ja/|東北大学電気通信研究所]] >> ソフトウェア構成研究室 |
| |
| English version is [[en|here]] | |
| |
| ====== ソフトウェア構成研究室 ====== | ====== ソフトウェア構成研究室 ====== |
| ===== 最新のニュース ===== | ===== 最新のニュース ===== |
| |
| * **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月**. **海野 広志**教授が東北大学に着任し、ソフトウェア構成研究室を設立しました。 |
| |
| ===== 研究室生活 ===== | ===== 研究室生活 ===== |
| |
| ^ 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)]] | |
