• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

海野 広志  UNNO HIROSHI

研究者番号 80569575
その他のID
  • ORCIDhttps://orcid.org/0000-0002-4225-8195
所属 (現在) 2025年度: 東北大学, 電気通信研究所, 教授
所属 (過去の研究課題情報に基づく) *注記 2024年度 – 2025年度: 東北大学, 電気通信研究所, 教授
2016年度 – 2023年度: 筑波大学, システム情報系, 准教授
2013年度 – 2016年度: 筑波大学, システム情報系, 助教
2015年度: 筑波大学, 大学院システム情報工学研究科, 助教
2012年度 – 2014年度: 筑波大学, システム情報工学研究科(系), 助教
審査区分/研究分野
研究代表者
ソフトウェア / 大区分J / 小区分60050:ソフトウェア関連
研究代表者以外
小区分60050:ソフトウェア関連 / ソフトウェア / 中区分60:情報科学、情報工学およびその関連分野 / 大区分J / 情報学基礎理論 / 情報学基礎
キーワード
研究代表者
関係的仕様 / プログラム検証 / プログラム合成 / 循環証明 / 述語制約解消 / 不動点論理 / 時相的仕様 / 帰納的定理証明 / ホーン節制約解消 / 依存型 … もっと見る / リファインメント型 / shift0/reset0 / CHC optimization / de Morgan双対性 / 再帰データ型 / 動的論理 / 述語充足可能性判定 / 不動点制約解消 / スコーレム関数 / ランキング関数 / 不変条件 / 時相的・関係的仕様 / 依存リファインメント型 / プログラミング言語 / 停止性検証 / 関係的仕様検証 / 抽象解釈 / トレース意味論 / ゲーム意味論 / 制約最適化 / 制約解消 / 定理自動証明 / 型システム … もっと見る
研究代表者以外
プログラム検証 / 型システム / プログラミング言語 / 高階モデル検査 / 機械学習 / 不動点論理 / 高階不動点論理 / モデル検査 / 代数的エフェクト / 自動定理証明 / 関数型プログラム / 高階文法 / データ圧縮 / 述語制約解消 / 述語制約 / 依存篩型 / システム検証 / CHCソルバ / 定理自動証明 / 演繹的推論 / 時相的検証 / 代数的効果ハンドラ / 並行・並列プログラム / 確率付き高階不動点論理 / 形式手法 / 強化学習 / IoT / PDR / モニタリング / ブラックボックス検査 / 形式検証 / ハイブリッドシステム / トレース意味論 / 非決定計算 / 顕在的契約計算 / 計算効果 / 漸進的型付け / プログラム論理 / ソフトウェアモデル検査 / 循環証明 / 分離論理 / 共通型 / 高階論理 / 確率付き文法 / ソフトウェア検証 / 実行時プログラム生成 / 関数型プログラミング言語 / 高性能計算 / プログラム特化 / プログラム変換 / プログラム生成 / 関数型プログラム言語 / ディペンダブルコンピューティング / 型理論 / 高階再帰スキーム / 関数型言語 隠す
  • 研究課題

    (15件)
  • 研究成果

    (81件)
  • 共同研究者

    (19人)
  •  プログラム検証技術の基礎付けと応用研究代表者

    • 研究代表者
      海野 広志
    • 研究期間 (年度)
      2025 – 2029
    • 研究種目
      基盤研究(S)
    • 審査区分
      大区分J
    • 研究機関
      東北大学
  •  並行・並列プログラミングのためのスケーラブルな自動プログラム検証技術

    • 研究代表者
      関山 太朗
    • 研究期間 (年度)
      2024 – 2027
    • 研究種目
      基盤研究(A)
    • 審査区分
      中区分60:情報科学、情報工学およびその関連分野
    • 研究機関
      国立情報学研究所
  •  機械学習技術による高速な演繹的推論エンジンの開発

    • 研究代表者
      塚田 武志
    • 研究期間 (年度)
      2022 – 2026
    • 研究種目
      基盤研究(B)
    • 審査区分
      小区分60050:ソフトウェア関連
    • 研究機関
      千葉大学
  •  依存篩型と述語制約によるプログラム検証の深化

    • 研究代表者
      寺内 多智弘
    • 研究期間 (年度)
      2022 – 2026
    • 研究種目
      基盤研究(B)
    • 審査区分
      小区分60050:ソフトウェア関連
    • 研究機関
      早稲田大学
  •  高階不動点論理に基づくプログラム検証

    • 研究代表者
      小林 直樹
    • 研究期間 (年度)
      2020
    • 研究種目
      基盤研究(A)
    • 審査区分
      中区分60:情報科学、情報工学およびその関連分野
    • 研究機関
      東京大学
  •  AI時代を見据えたプログラム検証技術

    • 研究代表者
      小林 直樹
    • 研究期間 (年度)
      2020 – 2024
    • 研究種目
      基盤研究(S)
    • 審査区分
      大区分J
    • 研究機関
      東京大学
  •  時相的・関係的仕様からの高レベルプログラム合成研究代表者

    • 研究代表者
      海野 広志
    • 研究期間 (年度)
      2020 – 2024
    • 研究種目
      基盤研究(B)
    • 審査区分
      小区分60050:ソフトウェア関連
    • 研究機関
      東北大学
      筑波大学
  •  IoT システムのための形式検証手法の深化

    • 研究代表者
      末永 幸平
    • 研究期間 (年度)
      2019 – 2023
    • 研究種目
      基盤研究(B)
    • 審査区分
      小区分60050:ソフトウェア関連
    • 研究機関
      京都大学
  •  高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証

    • 研究代表者
      寺内 多智弘
    • 研究期間 (年度)
      2017 – 2021
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウェア
    • 研究機関
      早稲田大学
  •  現代的なプログラミング言語のための漸進的型システムの理論

    • 研究代表者
      五十嵐 淳
    • 研究期間 (年度)
      2017 – 2020
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウェア
    • 研究機関
      京都大学
  •  高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証研究代表者

    • 研究代表者
      海野 広志
    • 研究期間 (年度)
      2016 – 2019
    • 研究種目
      若手研究(A)
    • 研究分野
      ソフトウェア
    • 研究機関
      筑波大学
  •  高階モデル検査の深化と発展

    • 研究代表者
      小林 直樹
    • 研究期間 (年度)
      2015 – 2019
    • 研究種目
      基盤研究(S)
    • 研究分野
      情報学基礎理論
    • 研究機関
      東京大学
  •  信頼性の高いコード生成のためのプログラミング言語の実現

    • 研究代表者
      亀山 幸義
    • 研究期間 (年度)
      2013 – 2015
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウェア
    • 研究機関
      筑波大学
  •  ゲーム意味論に基づくリファインメント型の拡張とその応用研究代表者

    • 研究代表者
      海野 広志
    • 研究期間 (年度)
      2013 – 2015
    • 研究種目
      若手研究(B)
    • 研究分野
      ソフトウェア
    • 研究機関
      筑波大学
  •  高階モデル検査とその応用

    • 研究代表者
      小林 直樹
    • 研究期間 (年度)
      2011 – 2015
    • 研究種目
      基盤研究(S)
    • 研究分野
      情報学基礎
    • 研究機関
      東京大学
      東北大学

すべて 2024 2023 2022 2021 2020 2019 2018 2017 2016 2015 2014 2013 2011 その他

すべて 雑誌論文 学会発表

  • [雑誌論文] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • 著者名/発表者名
      Kawamata Fuga, Unno Hiroshi, Sekiyama Taro, Terauchi Tachio
    • 雑誌名

      Proceedings of the ACM on Programming Languages (POPL)

      巻: 8 号: POPL ページ: 115-147

    • DOI

      10.1145/3633280

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H00582, KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-23K24826
  • [雑誌論文] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
    • 雑誌名

      In Proceedings of the 50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023), PACMPL 7(POPL)

      巻: 7 号: POPL ページ: 2111-2140

    • DOI

      10.1145/3571265

    • 査読あり / オープンアクセス / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K24826, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Optimal CHC Solving via Termination Proofs2023

    • 著者名/発表者名
      Gu Yu、Tsukada Takeshi、Unno Hiroshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 7 号: POPL ページ: 604-631

    • DOI

      10.1145/3571214

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023

    • 著者名/発表者名
      Sekiyama Taro、Unno Hiroshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 7 号: POPL ページ: 2079-2110

    • DOI

      10.1145/3571264

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-22K17875, KAKENHI-PROJECT-20H00582, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Software model-checking as cyclic-proof search2022

    • 著者名/発表者名
      Tsukada Takeshi、Unno Hiroshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 6 号: POPL ページ: 1-29

    • DOI

      10.1145/3498725

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Toward Neural-Network-Guided Program Synthesis and Verification2021

    • 著者名/発表者名
      Kobayashi Naoki、Sekiyama Taro、Sato Issei、Unno Hiroshi
    • 雑誌名

      Lecture Notes in Computer Science (SAS)

      巻: 12913 ページ: 236-260

    • DOI

      10.1007/978-3-030-88806-0_12

    • ISBN
      9783030888053, 9783030888060
    • 査読あり
    • データソース
      KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Constraint-Based Relational Verification2021

    • 著者名/発表者名
      Unno Hiroshi、Terauchi Tachio、Koskinen Eric
    • 雑誌名

      Proceedings of CAV 2021, Springer LNCS

      巻: 12759 ページ: 742-766

    • DOI

      10.1007/978-3-030-81685-8_35

    • ISBN
      9783030816841, 9783030816858
    • 査読あり / オープンアクセス / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Decision Tree Learning in CEGIS-Based Termination Analysis2021

    • 著者名/発表者名
      Kura Satoshi、Unno Hiroshi、Hasuo Ichiro
    • 雑誌名

      Proceedings of CAV 2021, Springer LNCS

      巻: 12760 ページ: 75-98

    • DOI

      10.1007/978-3-030-81688-9_4

    • ISBN
      9783030816872, 9783030816889
    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno, and Hinata Yanagi
    • 雑誌名

      Proceedings of the annual AAAI Conference on Artificial Intelligence (AAAI 2020)

      巻: 印刷中

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-16H05856
  • [雑誌論文] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • 著者名/発表者名
      Satake Yuki、Unno Hiroshi、Yanagi Hinata
    • 雑誌名

      Proceedings of the AAAI Conference on Artificial Intelligence

      巻: 34 号: 02 ページ: 1644-1651

    • DOI

      10.1609/aaai.v34i02.5526

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-15H05706
  • [雑誌論文] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno, and Hinata Yanagi
    • 雑誌名

      Proceedings of the annual AAAI Conference on Artificial Intelligence (AAAI 2020)

      巻: -

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-17H01723
  • [雑誌論文] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020

    • 著者名/発表者名
      KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
    • 雑誌名

      コンピュータ ソフトウェア

      巻: 37 号: 1 ページ: 1_39-1_52

    • DOI

      10.11309/jssst.37.1_39

    • NAID

      130007815024

    • ISSN
      0289-6540
    • 年月日
      2020-01-24
    • 言語
      日本語
    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
  • [雑誌論文] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno, Hinata Yanagi
    • 雑誌名

      In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020)

      巻: AAAI 2020 ページ: 1644-1651

    • 査読あり
    • データソース
      KAKENHI-PROJECT-17H01720
  • [雑誌論文] Temporal Verification of Programs via First-Order Fixpoint Logic2019

    • 著者名/発表者名
      Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
    • 雑誌名

      In Proceedings of the 26th International Symposium (SAS 2019), Lecture Notes in Computer Science

      巻: 11822 ページ: 413-436

    • DOI

      10.1007/978-3-030-32304-2_20

    • ISBN
      9783030323035, 9783030323042
    • 査読あり
    • データソース
      KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-15H05706
  • [雑誌論文] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs2018

    • 著者名/発表者名
      Hiroshi Unno, Yuki Satake, and Tachio Terauchi
    • 雑誌名

      Proceedings of the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018), PACMPL

      巻: 2 号: POPL ページ: 1-29

    • DOI

      10.1145/3158100

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723, KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-15H05706
  • [雑誌論文] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 雑誌名

      Proceedings of LICS 2018

      巻: 印刷中 ページ: 759-768

    • DOI

      10.1145/3209108.3209204

    • 査読あり / オープンアクセス / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720
  • [雑誌論文] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 雑誌名

      Proceedings of CAV 2018, LNCS

      巻: 印刷中

    • 査読あり
    • データソース
      KAKENHI-PROJECT-17H01723
  • [雑誌論文] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 雑誌名

      Proceedings of CAV 2018, LNCS

      巻: 印刷中

    • 査読あり
    • データソース
      KAKENHI-PROJECT-16H05856
  • [雑誌論文] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 雑誌名

      Proceedings of LICS 2018

      巻: 印刷中

    • 査読あり / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01723
  • [雑誌論文] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Satake Yuki、Unno Hiroshi
    • 雑誌名

      Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), Lecture Notes in Computer Science, Springer

      巻: 10981 ページ: 105-123

    • DOI

      10.1007/978-3-319-96145-3_6

    • ISBN
      9783319961446, 9783319961453
    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-17H01720
  • [雑誌論文] Automating Induction for Solving Horn Clauses2017

    • 著者名/発表者名
      Unno Hiroshi、Torii Sho、Sakamoto Hiroki
    • 雑誌名

      Proceedings of CAV 2017, Springer LNCS

      巻: 10427 ページ: 571-591

    • DOI

      10.1007/978-3-319-63390-9_30

    • ISBN
      9783319633893, 9783319633909
    • 査読あり
    • データソース
      KAKENHI-PROJECT-15H05706
  • [雑誌論文] Automating Induction for Solving Horn Clauses2017

    • 著者名/発表者名
      Hiroshi Unno, Sho Torii, Hiroki Sakamoto
    • 雑誌名

      Proceedings of CAV 2017, LNCS

      巻: 印刷中

    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-16H05856
  • [雑誌論文] Temporal Verification of Higher-Order Functional Programs2016

    • 著者名/発表者名
      Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
    • 雑誌名

      In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices

      巻: 51 (1) ページ: 57-68

    • DOI

      10.1145/2837614.2837667

    • 査読あり / 謝辞記載あり / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-25280020, KAKENHI-PROJECT-25280023
  • [雑誌論文] Refinement Type Inference via Horn Constraint Optimization2015

    • 著者名/発表者名
      Kodai Hashimoto, Hiroshi Unno
    • 雑誌名

      Proceedings of SAS 2015, LNCS

      巻: 9291 ページ: 199-216

    • DOI

      10.1007/978-3-662-48288-9_12

    • ISBN
      9783662482872, 9783662482889
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-25280020
  • [雑誌論文] Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs2015

    • 著者名/発表者名
      Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
    • 雑誌名

      Proceedings of CAV 2015, LNCS

      巻: 未定

    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-25730035
  • [雑誌論文] Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling2015

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi.
    • 雑誌名

      Proceedings of TACAS 2015, LNCS

      巻: 9035 ページ: 149-163

    • DOI

      10.1007/978-3-662-46681-0_10

    • ISBN
      9783662466803, 9783662466810
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-23220001
  • [雑誌論文] Verification of Tree-Processing Programs via Higher-Order Mode Checking2015

    • 著者名/発表者名
      Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
    • 雑誌名

      Mathematical Structures in Computer Science

      巻: Volume 25, Special Issue 04 号: 4 ページ: 841-866

    • DOI

      10.1017/s0960129513000054

    • 査読あり
    • データソース
      KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-23220001
  • [雑誌論文] 高階木変換器の自動検証のための反例発見と抽象化改良2015

    • 著者名/発表者名
      松本雄磨, 小林直樹, 海野広志
    • 雑誌名

      コンピュータ ソフトウェア

      巻: 32 号: 1 ページ: 1_161-1_178

    • DOI

      10.11309/jssst.32.1_161

    • NAID

      130004892316

    • ISSN
      0289-6540
    • 言語
      日本語
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-23220001
  • [雑誌論文] Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs2015

    • 著者名/発表者名
      Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
    • 雑誌名

      Proceedings of CAV 2015, LNCS

      巻: 9207 ページ: 287-303

    • DOI

      10.1007/978-3-319-21668-3_17

    • ISBN
      9783319216676, 9783319216683
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-23220001
  • [雑誌論文] Relaxed Stratication: A New Approach to Practical Complete Predicate Refinement2015

    • 著者名/発表者名
      Tachio Terauchi, Hiroshi Unno
    • 雑誌名

      Proceedings of ESOP 2015, LNCS

      巻: 9032 ページ: 610-633

    • DOI

      10.1007/978-3-662-46669-8_25

    • ISBN
      9783662466681, 9783662466698
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-23220001
  • [雑誌論文] Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs2015

    • 著者名/発表者名
      Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
    • 雑誌名

      Proceedings of APLAS 2015, LNCS

      巻: 9458 ページ: 295-312

    • DOI

      10.1007/978-3-319-26529-2_16

    • ISBN
      9783319265285, 9783319265292
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035
  • [雑誌論文] 高階木変換器の自動検証のための反例発見と抽象化改良2014

    • 著者名/発表者名
      松本 雄磨, 小林 直樹, 海野 広志
    • 雑誌名

      第 16 回プログラミングおよびプログラミング言語ワークショップ予稿集

      巻: - ページ: 1-18

    • NAID

      130004892316

    • 査読あり
    • データソース
      KAKENHI-PROJECT-25730035
  • [雑誌論文] Automatic Termination Verification for Higher-Order Functional Programs2014

    • 著者名/発表者名
      Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
    • 雑誌名

      Proceedings of ESOP 2014, LNCS

      巻: 8410 ページ: 392-411

    • DOI

      10.1007/978-3-642-54833-8_21

    • ISBN
      9783642548321, 9783642548338
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026, KAKENHI-PROJECT-25280023, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082
  • [雑誌論文] Automating relatively complete verification of higher-order functional programs2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
    • 雑誌名

      Proceedings of The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13

      巻: - ページ: 75-86

    • DOI

      10.1145/2429069.2429081

    • NAID

      120007136948

    • 査読あり
    • データソース
      KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026
  • [雑誌論文] Towards a scalable software model checker for higher-order programs2013

    • 著者名/発表者名
      Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
    • 雑誌名

      Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM 2013)

      巻: - ページ: 56-62

    • DOI

      10.1145/2426890.2426900

    • 査読あり
    • データソース
      KAKENHI-PROJECT-12J08057, KAKENHI-PROJECT-23220001
  • [雑誌論文] Predicate abstraction and CEGAR for higher-order model checking2011

    • 著者名/発表者名
      Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
    • 雑誌名

      Proceedings of the 32^<nd> ACM SIGPLAN conference on Programming language design and implementation (PLDI 2011)

      ページ: 222-233

    • DOI

      10.1145/1993498.1993525

    • 査読あり
    • データソース
      KAKENHI-PROJECT-23220001
  • [学会発表] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • 著者名/発表者名
      Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi
    • 学会等名
      ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
    • データソース
      KAKENHI-PROJECT-23K24826
  • [学会発表] 自動検証におけるラグランジュ双対性2024

    • 著者名/発表者名
      塚田 武志, 海野 広志
    • 学会等名
      第26回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-23K24820
  • [学会発表] Optimal CHC Solving via Termination Proofs2023

    • 著者名/発表者名
      Gu Yu、Tsukada Takeshi、Unno Hiroshi
    • 学会等名
      POPL 2023
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K20380
  • [学会発表] 代数的エフェクトハンドラのための篩型システム (ポスター発表)2023

    • 著者名/発表者名
      川俣 楓河, 海野 広志, 関山 太郎, 寺内 多智弘
    • 学会等名
      ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
    • データソース
      KAKENHI-PROJECT-23K24826
  • [学会発表] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023

    • 著者名/発表者名
      Unno Hiroshi、Terauchi Tachio、Gu Yu、Koskinen Eric
    • 学会等名
      POPL 2023
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K20380
  • [学会発表] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023

    • 著者名/発表者名
      Sekiyama Taro、Unno Hiroshi
    • 学会等名
      POPL 2023
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K20380
  • [学会発表] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2023

    • 著者名/発表者名
      Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
    • 学会等名
      NII Shonan Meeting Seminar 203:Effect Handlers and General-Purpose Languages
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K24826
  • [学会発表] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
    • 学会等名
      ソフトウェア科学会 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
    • データソース
      KAKENHI-PROJECT-23K24826
  • [学会発表] Constraint-Based Relational Verification2021

    • 著者名/発表者名
      Unno Hiroshi
    • 学会等名
      CAV 2021
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23K20380
  • [学会発表] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno, and Hinata Yanagi
    • 学会等名
      The annual AAAI Conference on Artificial Intelligence (AAAI 2020)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Propositional Dynamic Logic for Higher-Order Functional Programs2019

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Belief Propagation for Predicate Satisfiability Checking(ポスター発表)2019

    • 著者名/発表者名
      柳 日向, 海野 広志
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2019

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 学会等名
      Dagstuhl Seminar 19371: Deduction Beyond Satisfiability
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] On Cut-Elimination Theorem in Cyclic-Proof Systems2019

    • 著者名/発表者名
      Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] Temporal Verification of Programs via First-Order Fixpoint Logic2019

    • 著者名/発表者名
      NaokiKobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
    • 学会等名
      The 26th International Static Analysis Symposium (SAS 2019)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Solving First-Order Fixpoint Logic for Program Verification2019

    • 著者名/発表者名
      Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2019

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Horn Clauses and Beyond for Relational and Temporal Program Verification2018

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] 一階不動点論理の循環証明体系とプログラム検証への応用2018

    • 著者名/発表者名
      南條 陽史, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第35回大会
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Horn Clauses and Beyond for Relational and Temporal Program Verification2018

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS'18)
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01723
  • [学会発表] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 学会等名
      ACM/IEEE Symposium on Logic in Computer Science
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01723
  • [学会発表] On Cut-elimination in Cyclic Proof Systems2018

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01720
  • [学会発表] On Cut-elimination in Cycle Proof Systems(ポスター発表)2018

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      The 16th Asian Symposium on Programming Languages and Systems (APLAS'18)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 学会等名
      International Conference on Computer Aided Verification
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01723
  • [学会発表] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 学会等名
      ACM/IEEE Symposium on Logic in Computer Science
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Relatively complete refinement type system for verification of higher-order non-deterministic programs2018

    • 著者名/発表者名
      Hiroshi Unno, Yuki Satake, Tachio Terauchi
    • 学会等名
      ACM Symposium on Principles of Programming Languages
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-17H01723
  • [学会発表] Dependent Temporal Effects and Fixpoint Logic for Verification2018

    • 著者名/発表者名
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • 学会等名
      第20回プログラミングおよびプログラミング言語ワーク ショップ(PPL2018)
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Horn Clauses and Beyond for Relational and Temporal Program Verification2018

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS'18)
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 学会等名
      International Conference on Computer Aided Verification
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] 一階不動点論理の循環証明体系とプログラム検証への応用2018

    • 著者名/発表者名
      南條 陽史, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第35回大会
    • データソース
      KAKENHI-PROJECT-17H01723
  • [学会発表] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs2018

    • 著者名/発表者名
      Hiroshi Unno, Yuki Satake, Tachio Terauchi
    • 学会等名
      ACM Symposium on Principles of Programming Languages
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] On Cut-elimination in Cycle Proof Systems2018

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      The 4th Workshop on New Ideas and Emerging Results (NIER'18)
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] A Horn Constraint Solver based on Inductive Theorem Proving(ポスター発表)2017

    • 著者名/発表者名
      Hiroki Sakamoto, Sho Torii, Shu Nakao, Hiroshi Unno
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)
    • 発表場所
      華やぎの章 慶山(山梨県笛吹市)
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] 関係的仕様からの関数型プログラム合成2017

    • 著者名/発表者名
      中尾 收, 佐竹 佑規, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第34回大会
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] 余帰納法に基づく定理証明の自動化2017

    • 著者名/発表者名
      四宮 誠一, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第34回大会
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Temporal Logics for Higher-Order Functional Programs based on Trace Semantics(ポスター発表)2017

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)
    • 発表場所
      華やぎの章 慶山(山梨県笛吹市)
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Temporal Dependent Contracts for Higher-Order Functions2016

    • 著者名/発表者名
      佐竹 佑規, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第33回大会
    • 発表場所
      東北大学(宮城県仙台市)
    • データソース
      KAKENHI-PROJECT-16H05856
  • [学会発表] Relational Verification of Functional Programs via Induction-based Horn Constraint Solving2016

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      NII Shonan Meeting on Higher-Order Model Checking
    • 発表場所
      湘南国際村センター(神奈川県三浦郡)
    • 年月日
      2016-03-19
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-25730035
  • [学会発表] Refinement Caml: A Refinement Type Checking and Inference Tool for OCaml2016

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      Dagstuhl Seminar on Language Based Verification Tools for Functional Programs
    • 発表場所
      Wadern, Germany
    • 年月日
      2016-03-31
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-25730035
  • [学会発表] Higher-order Program Verification as Renement Type Inference2015

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      Workshop on Higher- Order Program Analysis (HOPA 2015)
    • 発表場所
      京都大学(京都府京都市)
    • 年月日
      2015-07-04
    • 招待講演 / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-25730035
  • [学会発表] Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types2015

    • 著者名/発表者名
      Hiroshi Unno
    • 学会等名
      NII Shonan Meeting on Semantics and Verification of Object-Oriented Languages
    • 発表場所
      湘南国際村センター(神奈川県三浦郡)
    • 年月日
      2015-09-21
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-25730035
  • [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs2013

    • 著者名/発表者名
      海野 広志
    • 学会等名
      日本ソフトウェア科学会創設30周年記念大会
    • 発表場所
      東京
    • 招待講演
    • データソース
      KAKENHI-PROJECT-25730035
  • [学会発表] 高階木変換器の自動検証のための反例発見と抽象化改良

    • 著者名/発表者名
      松本 雄磨、小林 直樹、海野 広志
    • 学会等名
      第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
    • 発表場所
      阿蘇の司 ビラパークホテル(熊本県阿蘇市)
    • 年月日
      2014-03-05 – 2014-03-07
    • データソース
      KAKENHI-PROJECT-23220001
  • 1.  五十嵐 淳 (40323456)
    共同の研究課題数: 7件
    共同の研究成果数: 0件
  • 2.  小林 直樹 (00262155)
    共同の研究課題数: 4件
    共同の研究成果数: 6件
  • 3.  寺内 多智弘 (70447150)
    共同の研究課題数: 4件
    共同の研究成果数: 15件
  • 4.  佐藤 亮介 (10804677)
    共同の研究課題数: 3件
    共同の研究成果数: 1件
  • 5.  関山 太朗 (80828476)
    共同の研究課題数: 3件
    共同の研究成果数: 3件
  • 6.  篠原 歩 (00226151)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 7.  末永 幸平 (70633692)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 8.  塚田 武志 (50758951)
    共同の研究課題数: 2件
    共同の研究成果数: 3件
  • 9.  住井 英二郎 (00333550)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 10.  松田 一孝 (10583627)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 11.  亀山 幸義 (10195000)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 12.  浅井 健一 (10262156)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 13.  キセリョーフ オレッグ (50754602)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 14.  馬谷 誠二 (40378831)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 15.  中澤 巧爾 (80362581)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 16.  池渕 未来 (70961796)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 17.  吉仲 亮 (80466424)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 18.  佐藤 一誠 (90610155)
    共同の研究課題数: 1件
    共同の研究成果数: 1件
  • 19.  南出 靖彦 (50252531)
    共同の研究課題数: 1件
    共同の研究成果数: 0件

URL: 

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi