海野広志

うんのひろし | Unno Hiroshi

所属機関・部署：
職名：教授
ホームページURL (1件)： https://www.riec.tohoku.ac.jp/~unno/

研究分野 (2件)：ソフトウェア , 情報学基礎論

研究キーワード (5件)：定理自動証明 , モデル検査 , 型システム , 形式検証 , プログラミング言語

競争的資金等の研究課題 (13件)：

全件表示

論文 (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

講演・口頭発表等 (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 Workshop on Higher-Order Program Analysis (HOPA 2015) 2015)

学位 (1件)：

所属学会 (2件)：

日本ソフトウェア科学会 , ACM

※　J-GLOBALの研究者情報は、researchmapの登録情報に基づき表示しています。登録・更新については、こちらをご覧ください。

海野 広志