寺内多智弘 (Tachio Terauchi) - マイポータル

基本情報

所属: 早稲田大学理工学術院基幹理工学部情報理工学科教授

学位: 博士(カリフォルニア大学バークレー校)
修士(カリフォルニア大学バークレー校)
学士(コロンビア大学)

研究者番号: 70447150
J-GLOBAL ID: 200901015211509541
researchmap会員ID: 6000003825

外部リンク: https://terauchi.w.waseda.jp/index-j.html

プログラミング言語分野の研究を行っています。特に、プログラムの正しさを正式かつ(できるだけ)自動的に検証する「プログラム検証」や正しいプログラムを自動生成する「プログラム合成」の研究、およびプログラム検証・合成技術のセキュリティへの応用に興味があります。加えて、型システム、数理論理学と(特に自動)定理証明、形式言語理論とオートマトン理論など基礎理論・基礎アルゴリズムに関する研究も行っています。

研究キーワード

研究分野

経歴

2017年10月 - 現在

早稲田大学, 理工学術院基幹理工学部情報理工学科, 教授
2014年4月 - 2017年9月

北陸先端科学技術大学院大学, 情報科学研究科, 教授
2011年4月 - 2014年3月

名古屋大学, 大学院情報科学研究科, 准教授
2007年1月 - 2011年3月

東北大学, 大学院情報科学研究科, 助教

学歴

2000年9月 - 2006年8月

カリフォルニア大学バークレー校, Department of Electrical Engineering and Computer Sciences, Computer Science Division
1996年9月 - 2000年5月

コロンビア大学, School of Engineering and Applied Science, Computer Science Major

委員歴

2020年4月 - 2024年3月

ソフトウェア科学会プログラミング論研究会, 運営委員
2023年 - 2024年

The 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024), Program Committee
2023年 - 2024年

The 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2024), Program Committee
2023年 - 2024年

The 45th ACM SIGPLAN Symposium on Programming Language Design and Implementation (PLDI 2024), Program Committee
2023年 - 2024年

The 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Program Committee
2023年 - 2024年

The 17th International Symposium on Functional and Logic Programming (FLOPS 2024), Program Committee
2023年 - 2024年

The 37th IEEE Computer Security Foundations Symposium (CSF 2024), Program Committee
2022年 - 2023年

NII Shonan Meeting Seminar 180: The Art of SAT, Co-Organizer
2022年 - 2023年

The 21st Asian Symposium on Programming Languages and Systems (APLAS 2023), SRC & Posters Selection Committee
2022年 - 2023年

The 21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023), Program Committee
2022年 - 2023年

The 3rd International Conference on Code Quality (ICCQ 2023), Program Committee
2022年 - 2023年

The 36th IEEE Computer Security Foundations Symposium (CSF 2023), Program Committee
2022年 - 2023年

The 32nd European Symposium on Programming (ESOP 2023), Program Committee
2018年4月 - 2022年3月

情報処理学会プログラミング研究会(PRO), 幹事
2021年 - 2022年

The 37th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2022), Program Committee
2021年 - 2022年

The 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022), Program Committee
2021年 - 2022年

The 35th IEEE Computer Security Foundations Symposium (CSF 2022), Program Committee
2021年 - 2022年

The 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), Program Committee
2021年 - 2022年

The 49th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2022), Program Committee
2020年 - 2021年

Israel Science Foundation, Research Grant Application Reviewer

もっとみる

受賞

2024年3月

論文賞, Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness, ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)

野上大成, 寺内多智弘
2023年3月

論文賞, 後方参照付正規表現の表現力について, ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)

野上大成, 寺内多智弘
2023年1月

Distinguished Paper Award, Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification, The 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)

Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
2022年10月

辻井重男セキュリティ論文賞大賞, Repairing DoS Vulnerability of Real-World Regexes, 日本セキュリティ・マネジメント学会

千田忠賢, 寺内多智弘
2022年3月

論文賞, 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト, ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)

川俣楓河, 寺内多智弘
2019年12月

早稲田大学リサーチアワード国際研究発信力, 早稲田大学

寺内多智弘
2017年4月

Nominee, The EASST Award for the Best ETAPS Paper Related to the Systematic and Rigorous Engineering of Software and Systems, Compositional Synthesis of Leakage Resilient Programs, European Association for Software Science and Technology

Arthur Blot, Masaki Yamamoto, Tachio Terauchi
2009年5月

第4回野口研究奨励賞, 情報処理学会東北支部

寺内多智弘
2008年3月

発表賞(一般), ソフトウェア科学会第10回プログラミングおよびプログラミング言語ワークショップ (PPL 2008)

寺内多智弘

論文

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi

Proceedings of the ACM on Programming Languages 8(POPL) 115-147 2024年1月査読有り
On the Expressive Power of Regular Expressions with Backreferences

Taisei Nogami, Tachio Terauchi

In Proceedings of the 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), Leibniz International Proceedings in Informatics (LIPIcs) 272, pp.71:1-71:15, Schloss Dagstuhl Leibniz-Zentrum für Informatik 2023年8月査読有り
代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

川俣楓河, 寺内多智弘

コンピュータソフトウェア 40(2) 2_19-2_48 2023年6月査読有り招待有り
Repairing Regular Expressions for Extraction

Nariyoshi Chida, Tachio Terauchi

Proceedings of the ACM on Programming Languages 7(PLDI) 1633-1656 2023年6月査読有り
On Lookaheads in Regular Expressions with Backreferences

Nariyoshi Chida, Tachio Terauchi

IEICE Transactions on Information and Systems E106.D(5) 959-975 2023年5月査読有り
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

Proceedings of the ACM on Programming Languages 7(POPL) 2111-2140 2023年1月査読有り
On Lookaheads in Regular Expressions with Backreferences

Nariyoshi Chida, Tachio Terauchi

In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Leibniz International Proceedings in Informatics (LIPIcs) 228, pp.15:1-15:18, Schloss Dagstuhl Leibniz-Zentrum für Informatik 2022年8月査読有り
Repairing DoS Vulnerability of Real-World Regexes

Nariyoshi Chida, Tachio Terauchi

In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), pp.2060-2077, IEEE Computer Society 2022年5月査読有り
Constraint-based Relational Verification

Hiroshi Unno, Tachio Terauchi, Eric Koskinen

In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742-766, Springer 2021年査読有り
Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation

Tachio Terauchi, Timos Antonopoulos

Journal of Computer Security 28(6) 607-634 2020年査読有り
Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

コンピュータソフトウェア 37(1) 1_39-1_52 2020年査読有り招待有り
Games for Security under Adaptive Adversaries.

Timos Antonopoulos, Tachio Terauchi

In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019), pp.216-229, IEEE Computer Society 2019年査読有り
A Formal Analysis of Timing Channel Security via Bucketing.

Tachio Terauchi, Timos Antonopoulos

In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science 11426, pp.29-50, Springer 2019年査読有り
A Fixpoint Logic and Dependent Effects for Temporal Property Verification.

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pp. 759-768, ACM 2018年査読有り
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs.

Hiroshi Unno, Yuki Satake, Tachio Terauchi

Proceedings of the ACM on Programming Languages 2(POPL) 12:1-12:29 2018年査読有り
Compositional Synthesis of Leakage Resilient Programs

Arthur Blot, Masaki Yamamoto, Tachio Terauchi

In Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science 10204, pp.277-297, Springer 2017年査読有り
Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei

In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices 52 (6), pp.362-375. ACM 2017年査読有り
Temporal Verification of Higher-order Functional Programs

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices 51 (1), pp.57-68, ACM. 2016年査読有り
Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling

Hiroshi Unno, Tachio Terauchi

In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), Lecture Notes in Computer Science 9035, pp.149-163, Springer 2015年査読有り
Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR

Tachio Terauchi

In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.128-144, Springer 2015年査読有り

もっとみる

講演・口頭発表等

Repairing DoS Vulnerability of Real-World Regexes

Tachio Terauchi

NII Shonan Meeting Seminar 159: Web Application Security 2024年3月招待有り
Repairing Regular Expressions for Extraction

Nariyoshi Chida, Tachio Terauchi

ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024) 2024年3月
Nested Data Type における多相再帰のための主要型付けを持つ型システム

川原知真, 寺内多智弘

ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024) 2024年3月
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi

ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024) 2024年3月
Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness

野上大成, 寺内多智弘

ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024) 2024年3月
Repairing DoS Vulnerability of Real-World Regexes

Tachio Terauchi

Technology Challenges in Non-Traditional Security 2023年10月招待有り
Applications of Program Verification and Synthesis Techniques to Security, from Non-Interference to ReDoS

Tachio Terauchi

Vietnam-Japan Autumn School on Cyber Security 2023年10月招待有り
Repairing DoS Vulnerability of Real-World Regexes

Tachio Terauchi

NII Shonan Meeting Seminar 180:The Art of SAT 2023年10月
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi

NII Shonan Meeting Seminar 203:Effect Handlers and General-Purpose Languages 2023年10月招待有り
Repairing DoS Vulnerability of Real-World Regexes

Nariyoshi Chida, Tachio Terauchi

第22回情報科学技術フォーラム（FIT2023） 2023年9月招待有り
On Lookaheads in Regular Expressions with Backreferences

Nariyoshi Chida, Tachio Terauchi

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
On Lookaheads in Regular Expressions with Backreferences (Poster Presentation)

Nariyoshi Chida, Tachio Terauchi

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
Nested Data Type における多相再帰の型推論手法 (ポスター発表)

川原知真, 寺内多智弘

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
代数的エフェクトハンドラのための篩型システム (ポスター発表)

川俣楓河, 海野広志, 関山太郎, 寺内多智弘

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
後方参照付正規表現の表現力について

野上大成, 寺内多智弘

ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 2023年3月
Repairing DoS Vulnerability of Real-World Regexes (from IEEE S&P 2022)

Nariyoshi Chida, Tachio Terauchi

2022年暗号と情報セキュリティワークショップ 2022年9月招待有り
Repairing DoS Vulnerability of Real-World Regexes

Nariyoshi Chida, Tachio Terauchi

ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022) 2022年3月
代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

川俣楓河, 寺内多智弘

ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022) 2022年3月
Constraint-based Relational Verification

Tachio Terauchi

Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021) 2021年10月招待有り

もっとみる

所属学協会

共同研究・競争的資金等の研究課題

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

日本学術振興会科学研究費助成事業基盤研究(B) 基盤研究(B) 2022年4月 - 2027年3月

寺内多智弘, 海野広志
数理論理手法と人工知能手法の融合に基づくマルウェアの自動意味理解

日本学術振興会科学研究費助成事業挑戦的研究(開拓) 挑戦的研究(開拓) 2020年7月 - 2026年3月

小川瑞史, NGUYEN MinhLe, 寺内多智弘, 関浩之
時相的・関係的仕様からの高レベルプログラム合成

日本学術振興会科学研究費助成事業基盤研究(B) 基盤研究(B) 2020年4月 - 2025年3月

海野広志, 南出靖彦, 寺内多智弘
高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証

日本学術振興会科学研究費助成事業基盤研究(B) 基盤研究(B) 2017年4月 - 2022年3月

寺内多智弘, 海野広志
サイドチャネル攻撃耐タンパ性のためのプログラム検証・プログラム合成技術

日本学術振興会科学研究費助成事業挑戦的研究(萌芽) 挑戦的研究(萌芽) 2018年6月 - 2021年3月

寺内多智弘
数理論理学とその応用の国際研究拠点形成

日本学術振興会研究拠点形成事業先端拠点形成型 2015年4月 - 2020年3月

石原哉
論理的ー形式的手法による情報セキュリティ研究ー暗号プロトコル検証と量的情報流解析

日本学術振興会二国間交流事業共同研究 (AYAMEプログラム) 2016年4月 - 2019年3月

岡田光弘
実用効率の振舞いに基づくソフトウェア検証の数理的構造

日本学術振興会二国間交流事業共同研究 2015年4月 - 2017年12月

結縁祥治
高階プログラミング言語で記述された大規模ソフトウェアの検証

日本学術振興会科学研究費助成事業基盤研究(C) 基盤研究(C) 2014年4月 - 2017年3月

寺内多智弘
高レベル言語で記述されたリアクティブシステムに対する実時間性質の検証

日本学術振興会科学研究費助成事業基盤研究(B) 基盤研究(B) 2013年4月 - 2017年3月

結縁祥治, 寺内多智弘
高階プログラムのための時相論理仕様検証

日本学術振興会外国人特別研究員(欧米短期)事業 2013年 - 2013年

寺内多智弘, Eric Koskinen
量的情報流の正確な検証

日本学術振興会科学研究費助成事業若手研究(B) 若手研究(B) 2011年 - 2013年

寺内多智弘
ソフトウェアの安全性向上のための型理論の深化と応用

日本学術振興会科学研究費助成事業基盤研究(A) 基盤研究(A) 2008年 - 2010年

小林直樹, 五十嵐淳, 住井英二郎, 松田一孝, 寺内多智弘
型理論と線形計画法によるマルチスレッドプログラムの安全性検証

日本学術振興会科学研究費助成事業若手研究(B) 若手研究(B) 2008年 - 2010年

寺内多智弘

寺内多智弘

基本情報

研究キーワード

研究分野

経歴

学歴

委員歴

受賞

論文

講演・口頭発表等

所属学協会

共同研究・競争的資金等の研究課題

メニュー

共著者の一覧