Differences

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

--- en [2026/06/23 09:18] – external edit 127.0.0.1
+++ en [2026/09/27 07:41] (current) – external edit 127.0.0.1
@@ Line 6: / Line 6: @@
 ===== 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 "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]].
 	* **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**. 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]].
 	* **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]].
@@ Line 22: / Line 31: @@
 	* **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**. 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]].
-	* **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 "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 118: / Line 127: @@
 ^ 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/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)]] |