Unno Hiroshi

Affiliation
Faculty of Engineering, Information and Systems
Official title
Associate Professor
Research fields
Software
Theory of informatics
Research keywords
プログラム合成
自動定理証明
制約解消
型システム
モデル検査
自動推論
形式手法
プログラミング言語
人工知能
プログラム検証
Research projects
依存篩型と述語制約によるプログラム検証の深化2022-04 -- 2027-03寺内 多智弘日本学術振興会/科学研究費補助金 基盤研究（B）
機械学習技術による高速な演繹的推論エンジンの開発2022-04 -- 2027-03塚田 武志日本学術振興会/科学研究費補助金 基盤研究(B)
メタ数理システムデザインプロジェクト2020-04 -- 2022-03蓮尾 一郎独立行政法人科学技術振興機構/JST Strategic Basic Research Programs ERATO
AI時代を見据えたプログラム検証技術2020-08 -- 2025-03小林 直樹Japan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research (S)
時相的・関係的仕様からの高レベルプログラム合成2020-04 -- 2025-03Hiroshi UnnoJapan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research (B)
IoT システムのための形式検証手法の深化2019-04 -- 2024-03末永 幸平Japan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research (B)
現代的なプログラミング言語のための漸進的型システムの理論2017-04 -- 2020-03五十嵐 淳日本学術振興会/Grant in Aid for Scientific Research (B)
高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証2017-04 -- 2022-03寺内 多智弘Japan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research (B)
高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証2016-04 -- 2020-03海野 広志Japan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research14,560,000Yen
高階モデル検査の深化と発展2015-05 -- 2020-03小林 直樹Japan Society of for the Promotion of Science/Grant-in-Aid for Scientific Research (S)
more...
Degree
2009-03博士（情報理工学）The University of Tokyo
Honors & Awards
2016筑波大学若手教員奨励賞
2014-03PPL2014 論文賞論文がPPL2014プログラム委員に最優秀と評価された
Articles
  • 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
    木村 大輔; 中澤 巧爾; 寺内 多智弘; 海野 広志
    Computer Software/37(1)/pp.39-52, 2020-02
    CiNii
  • 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
    Lecture Notes in Computer Science 10427 (Part II)/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
  • 代数的データ構造を扱う関数型プログラムの検証法
    岡本 大輔; 海野 広志
    日本ソフトウェア科学会第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
  • more...
Conference, etc.
  • 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
  • Temporal Verification of Higher-order Functional Programs
    Murase Akihiro; Terauchi Tachio; Kobayashi Naoki; Sato Ryosu...
    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
  • more...
Works
  • EHMTT Verifier
    Unno Hiroshi; Tabuchi Naoshi; Kobayashi Naoki
  • MoCHi: Software Model Checker for Higher-Order Functional Programs
    Unno Hiroshi; Sato Ryosuke; Kobayashi Naoki
Teaching
2022-04 -- 2022-08Computer Science Seminar BUniversity of Tsukuba.
2022-10 -- 2023-02Computer Science Seminar BUniversity of Tsukuba.
2022-10 -- 2023-02Computer Science Seminar BfUniversity of Tsukuba.
2022-10 -- 2023-02Seminar in Computer Science fUniversity of Tsukuba.
2022-10 -- 2023-02Research in Computer Science fUniversity of Tsukuba.
2022-10 -- 2023-02Research in Computer Science IfUniversity of Tsukuba.
2022-04 -- 2022-08Research in Computer Science IUniversity of Tsukuba.
2022-10 -- 2023-02Research in Computer Science IUniversity of Tsukuba.
2022-04 -- 2022-08Seminar in Computer Science sUniversity of Tsukuba.
2022-04 -- 2022-08Computer Science Seminar AUniversity of Tsukuba.
more...
Professional activities
2021-04 -- (current)Information Processing Society of JapanPRO研究運営委員会/運営委員
2021-04 -- (current)Information Processing Society of JapanPRO編集委員会/編集委員
2021-04 -- (current)JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGYプログラミング論研究会 運営委員会
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-03JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY第18回プログラミングおよびプログラミング言語ワークショップ/組織委員長
more...
University Management
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情報科学類学務委員委員
more...

(Last updated: 2022-06-19)