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

2023 年度 実績報告書

依存篩型と述語制約によるプログラム検証の深化

研究課題

研究課題/領域番号 22H03570
配分区分補助金
研究機関早稲田大学

研究代表者

寺内 多智弘  早稲田大学, 理工学術院, 教授 (70447150)

研究分担者 海野 広志  筑波大学, システム情報系, 准教授 (80569575)
研究期間 (年度) 2022-04-01 – 2027-03-31
キーワードプログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 述語制約解消 / 代数的エフェクト
研究実績の概要

代数的エフェクトハンドラを含むプログラムのための依存篩型によるプログラム検証手法について研究を行った。具体的には、これまでの型推論と述語制約解消による手法を、Answer Type Modificationという限定継続等コントロールエフェクトのための型システムの概念とうまく組み合わせることにより、世界初の代数的エフェクトハンドラの動作を正確に解析することのできる依存篩型システムを開発した。この研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Principles of Programming Languages(POPL)に採録された。

加えて、制約解消による文字列抽出のための正規表現の生成・修正に関する研究と、後方参照により拡張された正規表現の表現力に関する研究を行った。前者の研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Programming Language Design and Implementation(PLDI)に採録された。後者の研究は理論計算機科学分野の難関国際会議であるInternational Symposium on Mathematical Foundations of Computer Science(MFCS)に採録された。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は主に代数的エフェクトハンドラを含むプログラムのための依存篩型システムに関する研究を行い成果を得た。

また、述語制約解消と自動定理証明に関する研究としては、前年度に提案した双対性をうまく用いた解消解消・不動点論理のための自動定理手法について引き続き研究を行っており、こちらの研究もおおむね順調に進展している。

今後の研究の推進方策

引き続き述語制約および不動点論理に関する研究を行う。特に、前年度開発した、述語制約への帰着と不動点論理の双対性を用いた新たな不動点論理妥当性判定手法の応用および手法のさらなる深化を目指す。加えて、引き続き代数的エフェクトハンドラや多相再帰(polymorphic recursion)など型システムに関する研究を行う。

  • 研究成果

    (15件)

すべて 2024 2023

すべて 雑誌論文 (5件) (うち査読あり 5件、 オープンアクセス 5件) 学会発表 (10件) (うち国際学会 5件、 招待講演 5件)

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

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

      In Proceedings of the 51st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2024). PACMPL 8(POPL)

      巻: 8 ページ: 115~147

    • DOI

      10.1145/3633280

    • 査読あり / オープンアクセス
  • [雑誌論文] On the Expressive Power of Regular Expressions with Backreferences2023

    • 著者名/発表者名
      Taisei Nogami, Tachio Terauchi
    • 雑誌名

      In Proceedings of the 48th Mathematical Foundations of Computer Science (MFCS 2023), Leibniz International Proceedings in Informatics (LIPIcs) 272

      巻: LIPICS ページ: 71:1~71:15

    • DOI

      10.4230/LIPIcs.MFCS.2023.71

    • 査読あり / オープンアクセス
  • [雑誌論文] 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト2023

    • 著者名/発表者名
      川俣 楓河, 寺内 多智弘
    • 雑誌名

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

      巻: 40 ページ: 2_19~2_48

    • DOI

      10.11309/jssst.40.2_19

    • 査読あり / オープンアクセス
  • [雑誌論文] Repairing Regular Expressions for Extraction2023

    • 著者名/発表者名
      Nariyoshi Chida, Tachio Terauchi
    • 雑誌名

      In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), PACMPL 7(PLDI)

      巻: 7 ページ: 1633~1656

    • DOI

      10.1145/3591287

    • 査読あり / オープンアクセス
  • [雑誌論文] On Lookaheads in Regular Expressions with Backreferences2023

    • 著者名/発表者名
      Nariyoshi Chida, Tachio Terauchi
    • 雑誌名

      IEICE Transactions on Information and Systems E106-D (5)

      巻: 5 ページ: 959~975

    • DOI

      10.1587/transinf.2022edp70

    • 査読あり / オープンアクセス
  • [学会発表] Repairing DoS Vulnerability of Real-World Regexes2024

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      NII Shonan Meeting Seminar 159: Web Application Security
    • 国際学会 / 招待講演
  • [学会発表] Repairing Regular Expressions for Extraction2024

    • 著者名/発表者名
      Nariyoshi Chida, Tachio Terauchi
    • 学会等名
      ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
  • [学会発表] Nested Data Type における多相再帰のための主要型付けを持つ型システム2024

    • 著者名/発表者名
      川原 知真, 寺内 多智弘
    • 学会等名
      ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
  • [学会発表] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • 著者名/発表者名
      Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi
    • 学会等名
      ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
  • [学会発表] Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness2024

    • 著者名/発表者名
      野上 大成, 寺内 多智弘
    • 学会等名
      ソフトウェア科学会 第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
  • [学会発表] Repairing DoS Vulnerability of Real-World Regexes2023

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      Technology Challenges in Non-Traditional Security
    • 国際学会 / 招待講演
  • [学会発表] Applications of Program Verification and Synthesis Techniques to Security, from Non-Interference to ReDoS2023

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      Vietnam-Japan Autumn School on Cyber Security
    • 国際学会 / 招待講演
  • [学会発表] Repairing DoS Vulnerability of Real-World Regexes2023

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      NII Shonan Meeting Seminar 180:The Art of SAT
    • 国際学会
  • [学会発表] 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
    • 国際学会 / 招待講演
  • [学会発表] Repairing DoS Vulnerability of Real-World Regexes2023

    • 著者名/発表者名
      Nariyoshi Chida, Tachio Terauchi
    • 学会等名
      第22回情報科学技術フォーラム(FIT2023
    • 招待講演

URL: 

公開日: 2024-12-25  

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

Powered by NII kakenhi