海野 広志(ウンノ ヒロシ)

所属
システム情報系
職名
准教授
研究分野
ソフトウェア
情報学基礎理論
研究キーワード
プログラム合成
自動定理証明
制約解消
型システム
モデル検査
自動推論
形式手法
プログラミング言語
人工知能
プログラム検証
研究課題
依存篩型と述語制約によるプログラム検証の深化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-03PPL2014 論文賞論文が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
    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
  • さらに表示...
作品
  • EHMTT Verifier
    Unno Hiroshi; Tabuchi Naoshi; Kobayashi Naoki
  • MoCHi: Software Model Checker for Higher-Order Functional Programs
    Unno Hiroshi; Sato Ryosuke; Kobayashi Naoki
担当授業科目
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-052020 Workshop on Trends, Extensions, Applications and Semantics of Logic Programming / program committee member
2018-11 -- 2020-01ACM SIGPLAN Symposium on Principles of Programming Languages47th ACM SIGPLAN Symposium on Principles of Programming Languages / program committee member
2018-09 -- 2019-12Asian Symposium on Programming Languages and Systems17th 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-03CS セミナー世話人世話人取りまとめ
2020-04 -- 2021-03CSダイバーシティ・アクセシビリティ担当教員
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)