海野 広志(ウンノ ヒロシ)
- 所属
- システム情報系
- 職名
- 准教授
- 研究分野
ソフトウェア 情報学基礎理論 - 研究キーワード
プログラム合成 自動定理証明 制約解消 型システム モデル検査 自動推論 形式手法 プログラミング言語 人工知能 プログラム検証 - 研究課題
依存篩型と述語制約によるプログラム検証の深化 2022-04 -- 2027-03 寺内 多智弘 日本学術振興会/科学研究費補助金 基盤研究(B) 機械学習技術による高速な演繹的推論エンジンの開発 2022-04 -- 2027-03 塚田 武志 日本学術振興会/科学研究費補助金 基盤研究(B) メタ数理システムデザインプロジェクト 2020-04 -- 2022-03 蓮尾 一郎 独立行政法人科学技術振興機構/戦略的創造研究推進事業ERATO AI時代を見据えたプログラム検証技術 2020-08 -- 2025-03 小林 直樹 日本学術振興会/科学研究費補助金 基盤研究(S) 時相的・関係的仕様からの高レベルプログラム合成 2020-04 -- 2025-03 海野 広志 日本学術振興会/科学研究費補助金 基盤研究(B) IoT システムのための形式検証手法の深化 2019-04 -- 2024-03 末永 幸平 日本学術振興会/科学研究費補助金 基盤研究(B) 現代的なプログラミング言語のための漸進的型システムの理論 2017-04 -- 2020-03 五十嵐 淳 日本学術振興会/科学研究費補助金 基盤研究(B) 高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証 2017-04 -- 2022-03 寺内 多智弘 日本学術振興会/科学研究費補助金 基盤研究(B) 高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証 2016-04 -- 2020-03 海野 広志 日本学術振興会/科学研究費 若手研究(A) 14,560,000円 高階モデル検査の深化と発展 2015-05 -- 2020-03 小林 直樹 日本学術振興会/科学研究費補助金 基盤研究(S) さらに表示... - 取得学位
2009-03 博士(情報理工学) 東京大学 - 受賞
2016 筑波大学若手教員奨励賞 2014-03 PPL2014 論文賞 論文がPPL2014プログラム委員に最優秀と評価された - 論文
- Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Unno Hiroshi; Terauchi Tachio; Gu Yu; Koskinen Eric
Proceedings of the ACM on Programming Languages/7(POPL)/pp.72:2111-72:2140, 2023-01 - Temporal Verification with Answer-Effect Modification
Sekiyama Taro; Unno Hiroshi
Proceedings of the ACM on Programming Languages/7(POPL)/pp.71:2079-71:2110, 2023-01 - Optimal CHC Solving via Termination Proofs
Gu Yu; Tsukada Takeshi; Unno Hiroshi
Proceedings of the ACM on Programming Languages/7(POPL)/pp.21:604-21:631, 2023-01 - Software Model-Checking as Cyclic-Proof Search
Tsukada Takeshi; Unno Hiroshi
Proceedings of the ACM on Programming Languages/6(POPL)/pp.63:1-63:29, 2022-01 - Toward Neural-Network-Guided Program Synthesis and Verification
Kobayashi Naoki; Sekiyama Taro; Sato Issei; Unno Hiroshi
Proceedings of the 28th Static Analysis Symposium (SAS 2021)/pp.236-260, 2021-10 - Constraint-based Relational Verification
Unno Hiroshi; Terauchi Tachio; Koskinen Eric
Proceedings of CAV 2021, 2021-07 - Decision Tree Learning in CEGIS-Based Termination Analysis
Kura Satoshi; Unno Hiroshi; Hasuo Ichiro
Proceedings of CAV 2021, 2021-07 - 筑波大学における全学必修 のデータサイエンス教育
和田耕一; 佐久間淳; 平田 祥人; 福地一斗; 青砥隆仁; 五十嵐康彦; 今倉暁; Vasilache Simona Mi...
オペレーションズ・リサーチ/65(9)/pp.573-578, 2020-11 - Temporal Verification of Programs via First-Order Fixpoint Logic
Kobayashi Naoki; Nishikawa Takeshi; Igarashi Atsushi; Unn...
Proceedings of SAS 2019, 2019-10 - Probabilistic Inference for Predicate Constraint Satisfaction
Satake Yuki; Unno Hiroshi; Yanagi Hinata
Proceedings of AAAI 2020, 2020-02 - Failure of Cut-Elimination in Cyclic Proofs of Separation Logic
木村 大輔; 中澤 巧爾; 寺内 多智弘; 海野 広志
コンピュータソフトウェア/37(1)/pp.39-52, 2020-02 - Temporal Verification of Programs via First-Order Fixpoint Logic
Satake Yuki; Unno Hiroshi
SAS 2019, 2019-09 - 一階不動点論理の循環証明体系とプログラム検証への応用
南條 陽史; 海野 広志
日本ソフトウェア科学会第35回大会予稿集, 2018-08 - Failure of Cut-Elimination in Cyclic Proofs of Separation Logic
Kimura Daisuke; Nakazawa Koji; Terauchi Tachio; Unno Hir...
第21回プログラミングおよびプログラミング言語ワークショップ予稿集, 2019-03 - Horn Clauses and Beyond for Relational and Temporal Program Verification
Unno Hiroshi
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE/(278)/pp.2-2, 2018 - 余帰納法に基づく定理証明の自動化
四宮 誠一; 海野 広志
日本ソフトウェア科学会第34回大会予稿集, 2017-09 - 関係的仕様からの関数型プログラム合成
中尾 收; 佐竹 佑規; 海野 広志
日本ソフトウェア科学会第34回大会予稿集, 2017-09 - A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Nanjo Yoji; Unno Hiroshi; Koskinen Eric; Terauchi Tachio
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018-07 - Propositional Dynamic Logic for Higher-Order Functional Programs
Satake Yuki; Unno Hiroshi
Proceedings of the 30th International Conference on Computer Aided Verification, 2018-07 - Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Unno Hiroshi; Torii Sho; Sakamoto Hiroki
Proceedings of the ACM on Programming Languages/2(POPL)/pp.12:1-12:29, 2017-12 - Temporal Dependent Contracts for Higher-Order Functions
Yuki Satake; Unno Hiroshi
日本ソフトウェア科学会第33回大会予稿集, 2016-09 - Automating Induction for Solving Horn Clauses
Unno Hiroshi; Torii Sho; Sakamoto Hiroki
Proceedings of the 29th International Conference on Computer Aided Verification/pp.571-591, 2017-07 - Automating Well-Founded Induction for Horn Clause Solving
Torii Sho; Unno Hiroshi
日本ソフトウェア科学会第32回大会予稿集/pp.1-4, 2015-09 - Temporal Verification of Higher-order Functional Programs
Murase Akihiro; Terauchi Tachio; Kobayashi Naoki; Sato Ryosu...
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages/pp.57-68, 2016-01 - Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
Matsumoto Yuma; Kobayashi Naoki; Unno Hiroshi
Proceedings of the 13th Asian Symposium on Programming Languages and Systems/9458/pp.295-312, 2015-11 - さらに表示...
- Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
- 会議発表等
- Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Unno Hiroshi; Terauchi Tachio; Gu Yu; Koskinen Eric
POPL/2023-01-15--2023-01-21 - Temporal Verification with Answer-Effect Modification
Sekiyama Taro; Unno Hiroshi
POPL/2023-01-15--2023-01-21 - Optimal CHC Solving via Termination Proofs
Gu Yu; Tsukada Takeshi; Unno Hiroshi
POPL/2023-01-15--2023-01-21 - Software Model-Checking as Cyclic-Proof Search
Tsukada Takeshi; Unno Hiroshi
49th ACM Symposium on Principles of Programming Languages/2022-01-16--2022-01-28 - Toward Neural-Network-Guided Program Synthesis and Verification
Kobayashi Naoki; Sekiyama Taro; Sato Issei; Unno Hiroshi
Static Analysis Symposium (SAS 2021)/2021-10-17--2021-10-19 - Constraint-based Relational Verification
Unno Hiroshi; Terauchi Tachio; Koskinen Eric
33rd International Conference on Computer-Aided Verification/2021-07-18--2021-07-24 - Decision Tree Learning in CEGIS-Based Termination Analysis
Kura Satoshi; Unno Hiroshi; Hasuo Ichiro
33rd International Conference on Computer-Aided Verification/2021-07-18--2021-07-24 - Temporal Verification of Programs via First-Order Fixpoint Logic
Kobayashi Naoki; Nishikawa Takeshi; Igarashi Atsushi; Unn...
26th Static Analysis Symposium (SAS 2019)/2019-10-9--2019-10-11 - Probabilistic Inference for Predicate Constraint Satisfaction
Satake Yuki; Unno Hiroshi; Yanagi Hinata
The Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-20)/2020-02-07--2020-02-12 - 一階不動点論理の循環証明体系とプログラム検証への応用
南條 陽史; 海野 広志
日本ソフトウェア科学会第35回大会/2018-08-29--2018-08-31 - Failure of Cut-Elimination in Cyclic Proofs of Separation Logic
Kimura Daisuke; Nakazawa Koji; Terauchi Tachio; Unno Hir...
第21回プログラミングおよびプログラミング言語ワークショップ/2019-03-06--2019-03-08 - Horn Clauses and Beyond for Relational and Temporal Program Verification
Unno Hiroshi
5th Workshop on Horn Clauses for Verification and Synthesis (HCVS) held as a Satellite Event of the Federated Logic Conference (FLoC)/2018-07-13--2018-07-13 - Horn Clauses and Beyond for Relational and Temporal Program Verification
Unno Hiroshi
HCVS 2018: 5th Workshop on Horn Clauses for Verification and Synthesis/2018-07-13--2018-07-13 - 余帰納法に基づく定理証明の自動化
四宮 誠一; 海野 広志
日本ソフトウェア科学会第34回大会/2017-09-18--2017-09-21 - 関係的仕様からの関数型プログラム合成
中尾 收; 佐竹 佑規; 海野 広志
日本ソフトウェア科学会第34回大会/2017-09-18--2017-09-21 - A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Nanjo Yoji; Unno Hiroshi; Koskinen Eric; Terauchi Tachio
LICS 2018: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science/2018-07-09--2018-07-12 - Propositional Dynamic Logic for Higher-Order Functional Programs
Satake Yuki; Unno Hiroshi
CAV 2018: 30th International Conference on Computer Aided Verification/2018-07-14--2018-07-17 - Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Unno Hiroshi; Torii Sho; Sakamoto Hiroki
POPL 2018: 45th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages/2018-01-10--2018-01-12 - Temporal Dependent Contracts for Higher-Order Functions
Yuki Satake; Unno Hiroshi
日本ソフトウェア科学会第33回大会/2016-09-06--2016-09-09 - Automating Induction for Solving Horn Clauses
Unno Hiroshi; Torii Sho; Sakamoto Hiroki
CAV 2017: 29th International Conference on Computer Aided Verification/2017-07-22--2017-07-28 - Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types
Unno Hiroshi
NII Shonan Meeting on "Semantics and Verification of Object-Oriented Languages"/2015-09-20--2015-09-25 - Relational Verification of Functional Programs via Induction-based Horn Constraint Solving
Unno Hiroshi
NII Shonan Meeting on "Higher-Order Model Checking"/2016-03-14--2016-03-17 - Refinement Caml: A Refinement Type Checking and Inference Tool for OCaml
Unno Hiroshi
Dagstuhl Seminar on "Language Based Verification Tools for Functional Programs"/2016-03-28--2016-04-01 - Higher-order Program Verification as Refinement Type Inference
Unno Hiroshi
HOPA 2015: The 3rd Workshop on Higher-Order Program Analysis/2015-07-04--2015-07-04 - Automating Well-Founded Induction for Horn Clause Solving
Torii Sho; Unno Hiroshi
日本ソフトウェア科学会第32回大会/2015-09-08--2015-09-11 - さらに表示...
- Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
- 作品
- EHMTT Verifier
Unno Hiroshi; Tabuchi Naoshi; Kobayashi Naoki - MoCHi: Software Model Checker for Higher-Order Functional Programs
Unno Hiroshi; Sato Ryosuke; Kobayashi Naoki
- EHMTT Verifier
- 担当授業科目
2023-10 -- 2024-02 情報理工前期特別研究IIf 筑波大学 2023-07 -- 2023-08 計算と情報科学 筑波大学 2023-10 -- 2024-02 情報理工前期特別研究If 筑波大学 2023-04 -- 2023-08 情報理工前期特別研究Is 筑波大学 2023-04 -- 2023-08 情報理工前期特別研究IIs 筑波大学 2023-04 -- 2023-08 情報理工前期特別演習s 筑波大学 2023-10 -- 2024-02 情報理工後期特別研究f 筑波大学 2023-10 -- 2024-02 情報理工前期特別演習f 筑波大学 2023-10 -- 2024-02 コンピュータサイエンス特別演習B 筑波大学 2023-04 -- 2023-08 コンピュータサイエンス特別演習B 筑波大学 さらに表示... - 学協会等委員
2021-04 -- (現在) 情報処理学会 PRO研究運営委員会/運営委員 2021-04 -- (現在) 情報処理学会 PRO編集委員会/編集委員 2021-04 -- (現在) 日本ソフトウェア科学会 プログラミング論研究会 運営委員会 2020-03 -- 2021-03 日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ/プログラム共同委員長 2019-08 -- 2020-05 2020 Workshop on Trends, Extensions, Applications and Semantics of Logic Programming / program committee member 2018-11 -- 2020-01 ACM SIGPLAN Symposium on Principles of Programming Languages 47th ACM SIGPLAN Symposium on Principles of Programming Languages / program committee member 2018-09 -- 2019-12 Asian Symposium on Programming Languages and Systems 17th Asian Symposium on Programming Languages and Systems / program committee member 2017-04 -- 2018-03 日本ソフトウェア科学会 第20回プログラミングおよびプログラミング言語ワークショップ/プログラム委員 2016-04 -- 2017-03 日本ソフトウェア科学会 第19回プログラミングおよびプログラミング言語ワークショップ/組織委員 2015-04 -- 2016-03 日本ソフトウェア科学会 第18回プログラミングおよびプログラミング言語ワークショップ/組織委員長 さらに表示... - 学内管理運営業績
2021-04 -- 2023-03 CS セミナー世話人 世話人取りまとめ 2020-04 -- 2021-03 CSダイバーシティ・アクセシビリティ 担当教員 2019-04 -- 2021-03 全学ダイバーシティ・アクセシビリティ 担当教員 2019-04 -- 2021-03 情報特別演習 世話人 2019-04 -- 2021-03 情報科学類広報企画委員会 委員 2017-09 -- 2019-03 情報科学類教育用計算機システム仕様策定委員会 委員 2018-04 -- 2019-05 システム情報工学研究科広報委員会 委員 2018-04 -- 2020-03 収書専門委員会 委員 2018-04 -- 2020-03 附属図書館運営委員会 委員 2017-04 -- 2019-03 情報科学類学務委員 委員 さらに表示...
(最終更新日: 2023-05-10)