Differences

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

--- en [2026/06/16 20:12] – [SAT and SMT Solvers] admin
+++ en [2026/06/26 19:02] (current) – hiroshi_unno
@@ Line 7: / Line 7: @@
 ===== News =====
+	* **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]].
 	* **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.
@@ Line 22: / Line 24: @@
 	* **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)]].
 	* **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 106: / Line 108: @@
 | Professor | [[https://www.riec.tohoku.ac.jp/~unno/|Hiroshi Unno]] |
 | Assistant Professor | [[https://www.riec.tohoku.ac.jp/~eberhart/|Clovis Eberhart]] |
-| Postdoctoral Researcher | Kenji Saotome |
+| Postdoctoral Researcher | [[https://researchmap.jp/k_saotome?lang=en|Kenji Saotome]] |
 | Secretary | Kyoko Sagae |
 | Graduate Students | [[takuma_monma|Takuma Monma]] |
@@ Line 120: / Line 122: @@
 | | 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)]] |
 | | 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://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://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://doi.org/10.1007/978-3-032-22720-1_15|doi]] | A Category-Theoretic Framework for Dependent Effect Systems | Satoshi Kura, Marco Gaboardi, Taro Sekiyama, and Hiroshi Unno | [[https://etaps.org/2026/conferences/esop/|European Symposium on Programming (ESOP 2026)]] |
 | [[https://doi.org/10.1007/978-3-032-11176-0_20|doi]] [[https://arxiv.org/pdf/2509.08343/|arXiv]] | AP-observation Automata for Abstraction-based Verification of Continuous-time Systems | Sasinee Pruekprasert and Clovis Eberhart | [[https://ictac2025.digital-hub.sh/|International Colloquium on Theoretical Aspects of Computing (ICTAC 2025)]] |