| Next revision | Previous revision |
| en:start [2026/06/23 09:18] – created admin | en:start [2026/09/27 07:41] (current) – [News] hiroshi_unno |
|---|
| |
| ===== News ===== | ===== News ===== |
| | * **September 2026**. The research project "Development of a Bespoke Transaction Processing Engine," for which Professor **Hiroshi Unno** serves as a principal collaborator (Principal Investigator: Professor **Hideyuki Kawashima**), has been selected for funding under [[https://www.jst.go.jp/kisoken/cronos/en/index.html|JST CRONOS]]. |
| | * **September 2026**. Professor **Hiroshi Unno** received the Distinguished Research Award at [[https://ses.sigse.jp/2026/|SES 2026]]. |
| | * **August 2026**. The paper "Automated Safety Verification of Posterior Distributions of Probabilistic Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://2026.ijcai.org/|IJCAI 2026]]. |
| | * **July 2026**. **Shota Okada**, **Hiroya Watanabe**, **Kazuki Uehara**, and Assistant Professor **Clovis Eberhart** presented research posters and demonstrated our verification tools **Athena** and **Thrust** at [[https://www.online-opencampus.tnc.tohoku.ac.jp/english/index.html|Tohoku University Open Campus 2026]]. |
| | * **July 2026**. The paper "Lagrangian-Based Duality for Quantified SMT Algorithms" by Professor **Hiroshi Unno** et al. was presented at [[https://conferences.i-cav.org/2026/|CAV 2026]]. |
| | * **July 2026**. We participated in [[https://termcomp.github.io/Y2026/|Termination Competition 2026]] with **MuVal**, a verification tool developed in our laboratory. |
| | * **July 2026**. **Takuma Monma** presented "Probabilistic Loop Acceleration via a Quantitative Fixpoint Logic," joint work with Assistant Professor **Clovis Eberhart** and Professor **Hiroshi Unno**, at [[https://veriprop.github.io/2026/|VeriProP 2026]]. |
| | * **July 2026**. The paper "Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition" by Professor **Hiroshi Unno** et al. was presented at [[https://satisfiability.org/SAT26/|SAT 2026]]. |
| * **June 2026**. The paper "A Hierarchy of Supermartingales for ω-Regular Verification" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi26.sigplan.org/|PLDI 2026]]. | * **June 2026**. The paper "A Hierarchy of Supermartingales for ω-Regular Verification" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi26.sigplan.org/|PLDI 2026]]. |
| * **June 2026**. 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]]. | * **June 2026**. 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]]. |
| | * **June 2026**. The paper "Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://pldi26.sigplan.org/home/ARRAY-2026|ARRAY 2026]]. |
| * **May 2026**. Professor **Hiroshi Unno** gave a keynote talk at [[https://mvl.jpn.org/ISMVL2026/|ISMVL 2026]]. | * **May 2026**. Professor **Hiroshi Unno** gave a keynote talk at [[https://mvl.jpn.org/ISMVL2026/|ISMVL 2026]]. |
| * **April 2026**. 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. | * **April 2026**. 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. |
| * **April 2026**. 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]]. | * **April 2026**. 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]]. |
| | * **April 2026**. Project Researcher **Kenji Saotome** has joined our laboratory. |
| * **March 2026**. **Takuma Monma** and **Kazuki Uehara** have presented posters about their research at [[https://jssst-ppl.org/workshop/2026/|PPL 2026]]. | * **March 2026**. **Takuma Monma** and **Kazuki Uehara** have presented posters about their research at [[https://jssst-ppl.org/workshop/2026/|PPL 2026]]. |
| * **November 2025**. 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]]. | * **November 2025**. 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]]. |
| * **May 2025**. Assistant Professor **Clovis Eberhart** has joined our laboratory. | * **May 2025**. Assistant Professor **Clovis Eberhart** has joined our laboratory. |
| * **April 2025**. We participated in [[https://chc-comp.github.io/2025/|CHC-COMP 2025]] with **PCSat** and **MuCyc**, two CHC solvers developed in our laboratory. | * **April 2025**. We participated in [[https://chc-comp.github.io/2025/|CHC-COMP 2025]] with **PCSat** and **MuCyc**, two CHC solvers developed in our laboratory. |
| * **April 2025**. 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)]]. | * **April 2025**. 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-25K24739/|KAKENHI Grant-in-Aid for Scientific Research (S)]]. |
| * **February 2025**. 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]]. | * **February 2025**. 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]]. |
| * **January 2025**. 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]]. | * **January 2025**. 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]]. |
| * **January 2025**. 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]]. | * **January 2025**. 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]]. |
| * **January 2025**. 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]]. | * **January 2025**. 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]]. |
| |
| ^ Link ^ Title ^ Authors ^ Journal / Conference ^ | ^ Link ^ Title ^ Authors ^ Journal / Conference ^ |
| | | 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)]] | |
