Unno Hiroshi

うんのひろし | Unno Hiroshi

Affiliation and department：
Homepage URL (1)： https://www.riec.tohoku.ac.jp/~unno/

Research field (2)： Software , Information theory

Research keywords (5)： automated theorem proving , model checking , type systems , formal verification , programming languages

Research theme for competitive and other funds (13)：

2022 - 2027 Dependent refinement types and predicate constraints for program verification
2022 - 2027 機械学習技術による高速な演繹的推論エンジンの開発
2020 - 2025 Program Verification Techniques for the AI Era
2020 - 2025 Synthesis of High-Level Programs from Temporal and Relational Specifications
2019 - 2024 IoT システムのための形式検証手法の深化

Show all

Papers (41)：

Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. Proceedings of the ACM on Programming Languages. 2024. 8. POPL. 115-147
Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proceedings of the ACM on Programming Languages. 2023. 7. POPL. 2111-2140
Yu Gu, Takeshi Tsukada, Hiroshi Unno 0001. Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 2023. 7. POPL. 604-631
Taro Sekiyama, Hiroshi Unno 0001. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang. 2023. 7. POPL. 2079-2110
Takeshi Tsukada, Hiroshi Unno. Software model-checking as cyclic-proof search. Proceedings of the ACM on Programming Languages. 2022. 6. POPL. 1-29

ｍore...

Lectures and oral presentations (3)：

Horn Clauses and Beyond for Relational and Temporal Program Verifi cation
(The 5th Workshop on Horn Clauses for Veri fication and Synthesis 2018)
Tutorial: Applications of Higher-order Model Checking to Program Verifi cation
(Workshop on Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS), 2016)
Higher-order Program Verifi cation as Refi nement Type Inference
(The 3rd Work- shop on Higher-Order Program Analysis (HOPA 2015) 2015)

Professional career (1)：

Association Membership(s) (2)：

JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY , ACM

※ Researcher’s information displayed in J-GLOBAL is based on the information registered in researchmap. For details, see here.

Return to Previous Page