ホーム > 海野 広志/ Unno, Hiroshi
海野 広志
ALUMNI
2025年4月現在、筑波大学が主たる所属機関ではありません
Unno, Hiroshi
東北大学 , 電気通信研究所 , 教授 Tohoku University , Research Institute of Electrical Communication
オープンアクセス版の論文は「つくばリポジトリ」で読むことができます。
-
1.
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
Taro Sekiyama; Hiroshi Unno
Proceedings of the ACM on Programming Languages 9: 2306 (2025)
-
2.
A Primal-Dual Perspective on Program Verification Algorithms
Takeshi Tsukada; Hiroshi Unno; Oded Padon; Sharon Shoham
Proceedings of the ACM on Programming Languages 9: 2025 (2025)
-
3.
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
Taro Sekiyama; Hiroshi Unno
Proceedings of the ACM on Programming Languages 8: 2662 (2024) Semantic Scholar
-
4.
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura; Hiroshi Unno
Proceedings of the ACM on Programming Languages 8: 973 (2024)
-
5.
Inductive Approach to Spacer
Takeshi Tsukada; Hiroshi Unno
Proceedings of the ACM on Programming Languages 8: 1979 (2024) Semantic Scholar
-
6.
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata; Hiroshi Unno; Taro Sekiyama; Tachio Terauchi
Proceedings of the ACM on Programming Languages 8: 115 (2024) Semantic Scholar
-
7.
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Hiroshi Unno; Tachio Terauchi; Yu Gu; Eric Koskinen
Proceedings of the ACM on Programming Languages 7: 2111 (2023) Semantic Scholar
-
8.
Optimal CHC Solving via Termination Proofs.
Yu Gu; Takeshi Tsukada; Hiroshi Unno 0001
Proc. ACM Program. Lang. 7: 604 (2023) Semantic Scholar
-
9.
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.
Taro Sekiyama; Hiroshi Unno 0001
Proc. ACM Program. Lang. 7: 2079 (2023) Semantic Scholar
-
10.
Software model-checking as cyclic-proof search
Takeshi Tsukada; Hiroshi Unno
Proceedings of the ACM on Programming Languages 6: 1 (2022) Semantic Scholar
-
11.
Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura; Hiroshi Unno; Ichiro Hasuo
Computer Aided Verification 75 (2021) Semantic Scholar
-
12.
Constraint-Based Relational Verification
Hiroshi Unno; Tachio Terauchi; Eric Koskinen
Computer Aided Verification 742 (2021) Semantic Scholar
-
13.
Toward Neural-Network-Guided Program Synthesis and Verification.
Naoki Kobayashi 0001; Taro Sekiyama; Issei Sato; Hiroshi Unno 0001
CoRR abs/2103.09414: (2021)
-
14.
Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
Takeshi Tsukada; Hiroshi Unno 0001; Taro Sekiyama; Kohei Suenaga
CoRR abs/2107.09766: (2021)
-
15.
Decision Tree Learning in CEGIS-Based Termination Analysis.
Satoshi Kura; Hiroshi Unno 0001; Ichiro Hasuo
CoRR abs/2104.11463: (2021)
-
16.
Toward Neural-Network-Guided Program Synthesis and Verification.
Naoki Kobayashi 0001; Taro Sekiyama; Issei Sato; Hiroshi Unno 0001
Static Analysis - 28th International Symposium(SAS) 236 (2021) Semantic Scholar
-
17.
Probabilistic Inference for Predicate Constraint Satisfaction
Yuki Satake; Hiroshi Unno; Hinata Yanagi
Proceedings of AAAI 2020 (2020)
-
18.
Failure of Cut-Elimination in Cyclic Proofs of Separation Logic
KIMURA Daisuke; NAKAZAWA Koji; TERAUCHI Tachio; UNNO Hiroshi
Computer Software 37: 1_39 (2020) Semantic Scholar
-
19.
Temporal Verification of Programs via First-Order Fixpoint Logic
Naoki Kobayashi; Takeshi Nishikawa; Atsushi Igarashi; Hiroshi Unno
Proceedings of SAS 2019 Springer LNCS 11822: 413 (2019) Semantic Scholar
-
20.
Relatively complete refinement type system for verification of higher-order non-deterministic programs
Hiroshi Unno; Yuki Satake; Tachio Terauchi
PACMPL 2: 12:1 (2018) Semantic Scholar
書籍等出版物情報はまだありません。
-
1.
Automating Relational Verification of Infinite-State Programs
25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024) 2024年1月16日 招待有り
-
2.
Constraint-based Relational Verification
38th International Conference on Mathematical Foundations of Programming Semantics 2022年7月13日 招待有り
-
3.
Horn Clauses and Beyond for Relational and Temporal Program Verification
海野 広志
The 5th Workshop on Horn Clauses for Verification and Synthesis 2018年7月13日 招待有り
-
4.
Tutorial: Applications of Higher-order Model Checking to Program Verification
海野 広志
Workshop on Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS), 2016年9月20日 招待有り
-
5.
Higher-order Program Verification as Refinement Type Inference
海野 広志
The 3rd Workshop on Higher-Order Program Analysis (HOPA 2015) 2015年7月4日 招待有り
知財情報はまだありません。
390 total views