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-03 Hiroshi Unno Japan 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 Research 14,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-03 PPL2014 論文賞 論文が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 - 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...
- Software Model-Checking as Cyclic-Proof Search
- 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...
- Software Model-Checking as Cyclic-Proof Search
- Works
- 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
- Teaching
2022-04 -- 2022-08 Computer Science Seminar B University of Tsukuba. 2022-10 -- 2023-02 Computer Science Seminar B University of Tsukuba. 2022-10 -- 2023-02 Computer Science Seminar Bf University of Tsukuba. 2022-10 -- 2023-02 Seminar in Computer Science f University of Tsukuba. 2022-10 -- 2023-02 Research in Computer Science f University of Tsukuba. 2022-10 -- 2023-02 Research in Computer Science If University of Tsukuba. 2022-04 -- 2022-08 Research in Computer Science I University of Tsukuba. 2022-10 -- 2023-02 Research in Computer Science I University of Tsukuba. 2022-04 -- 2022-08 Seminar in Computer Science s University of Tsukuba. 2022-04 -- 2022-08 Computer Science Seminar A University of Tsukuba. more... - Professional activities
2021-04 -- (current) Information Processing Society of Japan PRO研究運営委員会/運営委員 2021-04 -- (current) Information Processing Society of Japan PRO編集委員会/編集委員 2021-04 -- (current) JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY プログラミング論研究会 運営委員会 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 JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY 第18回プログラミングおよびプログラミング言語ワークショップ/組織委員長 more... - University Management
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 情報科学類学務委員 委員 more...
(Last updated: 2022-06-19)