現在地

海野 広志(ウンノ ヒロシ; Unno, Hiroshi)

face
所属
システム情報系
職名
准教授
研究分野
ソフトウェア
情報学基礎理論
研究キーワード
プログラム合成
自動定理証明
制約解消
型システム
モデル検査
自動推論
形式手法
プログラミング言語
人工知能
プログラム検証
研究課題
メタ数理システムデザインプロジェクト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)
高階モデル検査とその応用2012-08 -- 2016-03小林 直樹日本学術振興会/科学研究費補助金 基盤研究(S)2,600,000円
ゲーム意味論に基づくリファインメント型の拡張とその応用2013-04 -- 2016-03海野 広志日本学術振興会/科学研究費 若手研究(B)4,160,000円
取得学位
2009-03博士(情報理工学)東京大学
受賞
2016筑波大学若手教員奨励賞
2014-03PPL2014 論文賞論文がPPL2014プログラム委員に最優秀と評価された
論文
  • 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
  • 筑波大学における全学必修 のデータサイエンス教育
    和田耕一; 佐久間淳; 平田 祥人; 福地一斗; 青砥隆仁; 五十嵐...
    オペレーションズ・リサーチ/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 Hiroshi
    第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 Ry...
    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
  • 代数的データ構造を扱う関数型プログラムの検証法
    岡本 大輔; 海野 広志
    日本ソフトウェア科学会第31回大会予稿集, 2014-07
  • Refinement Type Inference via Horn Constraint Optimization
    Hashimoto Kodai; Unno Hiroshi
    Proceedings of the 22nd International Static Analysis Symposium/9291/pp.199-216, 2015-09
  • Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs
    Kuwahara Takuya; Sato Ryosuke; Unno Hiroshi; Kobayashi Naoki
    Proceedings of the 27th International Conference on Computer Aided Verification, 2015-07
  • Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
    Terauchi Tachio; Unno Hiroshi
    Proceedings of the 24th European Symposium on Programming/9032/pp.610-633, 2015-04
  • Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling
    Unno Hiroshi; Terauchi Tachio
    Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems/pp.149-163, 2015-04
会議発表等
  • 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 Hiroshi
    第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
  • Temporal Verification of Higher-order Functional Programs
    Murase Akihiro; Terauchi Tachio; Kobayashi Naoki; Sato Ry...
    POPL 2016: 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages/2016-01-20--2016-01-23
  • Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
    Matsumoto Yuma; Kobayashi Naoki; Unno Hiroshi
    APLAS 2015: 13th Asian Symposium on Programming Languages and Systems/2015-11-30--2015-12-02
  • 代数的データ構造を扱う関数型プログラムの検証法
    岡本 大輔; 海野 広志
    日本ソフトウェア科学会第31回大会/2014-09-07--2014-09-10
  • Automating Relatively Complete Verification of Higher-Order Functional Programs
    Unno Hiroshi; Terauchi Tachio; Kobayashi Naoki
    日本ソフト ウェア科学会創設30 周年記念大会/2013-9-10--2013-9-13
  • Refinement Type Inference via Horn Constraint Optimization
    Hashimoto Kodai; Unno Hiroshi
    SAS 2015: 22nd International Static Analysis Symposium/2015-09-09--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
担当授業科目
2021-10 -- 2022-02情報理工前期特別研究If筑波大学
2021-10 -- 2022-02情報理工後期特別演習Bf筑波大学
2021-04 -- 2021-08情報理工前期特別研究IIs筑波大学
2021-10 -- 2022-02情報理工前期特別演習f筑波大学
2021-04 -- 2021-08コンピュータサイエンス特別演習筑波大学
2021-10 -- 2022-02コンピュータサイエンス特別演習筑波大学
2021-10 -- 2022-02情報理工後期特別研究f筑波大学
2021-10 -- 2022-02コンピュータサイエンス特別研究I筑波大学
2021-04 -- 2021-08コンピュータサイエンス特別研究I筑波大学
2021-10 -- 2022-02情報理工後期特別演習Af筑波大学
学協会等委員
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情報科学類学務委員委員

(最終更新日: 2021-06-25)