[English Version]

寺内 多智弘

教授
早稲田大学 理工学術院 基幹理工学部 情報理工学科
03-5286-3198 (大学内内線 73-3805)
terauchi AT waseda DOT jp
[Researchmap.jp, 早稲田大学研究者データベース]

略歴

• 2000.5 コロンビア大学 卒業
• 2004.5 カリフォルニア大学バークレー校 修士号取得
• 2006.12 カリフォルニア大学バークレー校 博士号取得
• 2007.1-2011.3 東北大学 大学院情報科学研究科 助教
• 2011.4-2014.3 名古屋大学 大学院情報科学研究科 准教授
• 2014.4-2017.9 北陸先端科学技術大学院大学 情報科学研究科 教授
• 2017.10-現在 早稲田大学 情報理工学科 教授

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

講義

• プログラミング言語 (秋学期)
• プログラミング言語特論 (秋学期)
• 情報通信基礎 (春学期)
• プログラミングA (春学期)

研究室紹介

• 学生向け研究室紹介のページ
• 基幹理工学部Close Up記事
• 研究室説明会スライド
• プロジェクト研究A/B紹介スライド
• 研究室配属に関する面談を受け付けます。メールを送ってください。
• 場所：62号館W棟209B (希望があればオンラインでの面談も受け付けます。)

学会活動等

• CSF 2025 : プログラム委員
• POPL 2025 : プログラム委員
• ATVA 2024 : プログラム委員
• FMCAD 2024 : プログラム委員
• PLDI 2024 : プログラム委員
• FSCD 2024 : プログラム委員
• FLOPS 2024 : プログラム委員
• CSF 2024 : プログラム委員
• NII湘南会議 180 : 共同主催者
• APLAS 2023 : SRC & Posters Selection Committee
• ATVA 2023 : プログラム委員
• ICCQ 2023 : プログラム委員
• CSF 2023 : プログラム委員
• ESOP 2023 : プログラム委員
• OOPSLA 2022 : プログラム委員
• PLDI 2022 : プログラム委員
• CSF 2022 : プログラム委員
• LICS 2022 : プログラム委員
• POPL 2022 : プログラム委員
• TMPA 2021 : プログラム委員
• APLAS 2021 : プログラム委員
• ATVA 2021 : プログラム委員
• CAV 2021 : プログラム委員
• CSF 2021 : プログラム委員
• VSTTE 2020 : プログラム委員
• ATVA 2020 : プログラム委員
• FLOPS 2020 : プログラム委員
• PPL 2020 : プログラム委員
• TMPA 2019 : プログラム委員
• APLAS 2019 : プログラム委員
• ATVA 2019 : プログラム委員
• SAS 2019 : プログラム委員
• VSTTE 2019 : プログラム委員
• APLAS 2018 : プログラム委員
• VSTTE 2018 : プログラム委員
• NII湘南会議 115 : 共同主催者
• POPL 2018 : プログラム委員
• VMCAI 2018 : プログラム委員
• APLAS 2017 : プログラム委員
• RP 2017 : プログラム委員
• VSTTE 2017 : プログラム委員
• ESOP 2017 : プログラム委員
• TMPA 2017 : プログラム委員
• POPL 2017 : ERC委員
• APLAS 2016 : プログラム委員
• ICALP 2016 : プログラム委員
• VMCAI 2016 : プログラム委員
• POPL 2016 : ERC委員
• NII湘南会議 069 : 共同主催者
• HOPA 2015 : プログラム委員
• PLAS 2015 : プログラム委員
• LICS 2015 : プログラム委員
• FCS-FCC 2014 : プログラム委員
• HOPA 2014 : プログラム委員
• FLOPS 2014 : プログラム委員
• VMCAI 2014 : プログラム委員
• CSL 2013 : プログラム委員
• POPL 2013 : ERC委員
• APLAS 2012 : プログラム委員
• POPL 2012 : プログラム委員
• TLCA 2011 : プログラム委員
• ESOP 2011 : プログラム委員
• PLPV 2011 : プログラム委員
• VMCAI 2011 : プログラム委員
• TLDI 2011 : プログラム委員
• PLDI 2010 : ERC委員
• PPL 2010 : プログラム共同委員長
• PLAS 2009 : プログラム委員
• PPL 2009 : プログラム委員
• SAC 2009 : プログラム委員
• SAS 2008 : プログラム委員

学生指導

• 千田 忠賢 (客員研究員)
• Tianrui Chen (D1)
• 遠藤 龍之介 (M2)
• 富家 功一朗 (M2)
• 野上 大成 (M2)
• 山田 利樹 (M2)
• 川原 知真 (M1)
• 内城 勇太 (M1)
• 穴田 直也 (M1)
• 木村 海斗 (B4)
• 中山 祐貴 (B4)
• 飯田 大晟 (B4)
• 尾田 莉瑠 (B3)

論文 [Google Scholar, Semantic Scholar, DBLP]

• Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, and Tachio Terauchi.
  Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.
  In Proceedings of the 51st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2024). PACMPL 8(POPL): pp.115-147, ACM, Jan, 2024.
  [pdf (Full version with appendices)]
  


• Taisei Nogami and Tachio Terauchi.
  On the Expressive Power of Regular Expressions with Backreferences.
  In Proceedings of the 48th 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, August, 2023.
  [pdf (Full version with appendices)]
  


• Nariyoshi Chida and Tachio Terauchi.
  Repairing Regular Expressions for Extraction.
  In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), PACMPL 7(PLDI): pp.1633-1656, ACM, June, 2023.
  [pdf (Full version with appendices)]
  


• Nariyoshi Chida and Tachio Terauchi.
  On Lookaheads in Regular Expressions with Backreferences. (Extended Version)
  IEICE Transactions on Information and Systems E106-D (5), pp.959-975, (2023).
  


• 川俣楓河, 寺内多智弘.
  代数的エフェクトハンドラを持つ言語のためのトレースエフェクト.
  コンピュータソフトウェア 40 (2), pp.19-48, (2023).
  


• Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen.
  Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.
  In Proceedings of the 50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023), PACMPL 7(POPL): pp.2111-2140, ACM, January, 2023.
  [pdf (Full version with appendices)]
  


• Nariyoshi Chida and Tachio Terauchi.
  On Lookaheads in Regular Expressions with Backreferences.
  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, August, 2022.
  [pdf]
  


• Nariyoshi Chida and Tachio Terauchi.
  Repairing DoS Vulnerability of Real-World Regexes.
  In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), IEEE Computer Society, pp.2060-2077, May, 2022.
  [pdf (With bug fixes), Notes on a claim made by Li et al. USENIX Security 2022]
  


• Hiroshi Unno, Tachio Terauchi, and Eric Koskinen.
  Constraint-based Relational Verification.
  In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742-766, Springer, July, 2021.
  [pdf (Full version with appendices)]
  


• Tachio Terauchi and Timos Antonopoulos.
  Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation.
  Journal of Computer Security 28 (6): pp.607-634 (2020).
  [pdf]
  


• Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno.
  Failure of Cut-Elimination in Cyclic Proofs of Separation Logic.
  コンピュータソフトウェア 37 (1), pp.39-52, (2020).
  [pdf]
  


• Timos Antonopoulos and Tachio Terauchi.
  Games for Security under Adaptive Adversaries.
  In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019), pp.216-229, IEEE Computer Society, June, 2019.
  [pdf]
  


• Tachio Terauchi and Timos Antonopoulos.
  A Formal Analysis of Timing Channel Security via Bucketing.
  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, April, 2019.
  [pdf (With bug fixes)]
  


• Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi.
  A Fixpoint Logic and Dependent Effects for Temporal Property Verification
  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pp. 759-768, ACM, July, 2018.
  [pdf]
  


• Hiroshi Unno, Yuki Satake, and Tachio Terauchi.
  Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs.
  In Proceedings of the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018), PACMPL 2(POPL): pp.12:1-12:29, ACM, January, 2018.
  [pdf]
  


• Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei.
  Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels.
  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, June, 2017.
  [pdf]
  


• Arthur Blot, Masaki Yamamoto, and Tachio Terauchi.
  Compositional Synthesis of Leakage Resilient Programs.
  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, April, 2017.
  [pdf (Full version with proofs)]
  


• Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno.
  Temporal Verification of Higher-Order Functional Programs.
  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, January, 2016.
  [pdf]
  


• Tachio Terauchi.
  Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR.
  In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.128-144, Springer, September, 2015.
  [pdf (Full version with proofs)]
  


• Hiroshi Unno and Tachio Terauchi.
  Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling.
  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, April, 2015.
  [pdf (Full version with proofs)]
  


• Tachio Terauchi and Hiroshi Unno.
  Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement.
  In Proceedings of the 24th European Symposium on Programming (ESOP 2015), Lecture Notes in Computer Science 9032, pp.610-633, Springer, April, 2015.
  [pdf (Full version with proofs), experiment data]
  


• Eric Koskinen and Tachio Terauchi.
  Local Temporal Reasoning.
  In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), pp.59:1-59:10, ACM, July, 2014.
  [pdf (Full version with proofs)]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  Quantitative Information Flow as Safety and Liveness Hyperproperties. (Extended Version)
  Theoretical Computer Science 538: pp.167-182 (2014).
  


• Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi.
  Automatic Termination Verification for Higher-Order Functional Programs.
  In Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 8410, pp.392-411, Springer, April, 2014.
  [pdf (Full version with proofs)]
  


• 岩塚卓弥, 寺内多智弘, 結縁祥治.
  無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて.
  情報処理学会論文誌プログラミング(PRO) 6 (3): pp.20-32 (2013).
  


• Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi.
  Automating Relatively Complete Verification of Higher-Order Functional Programs.
  In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), ACM SIGPLAN Notices 48 (1), pp.75-86, ACM, January, 2013.
  [pdf (Full version with proofs)]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  Quantitative Information Flow as Safety and Liveness Hyperproperties.
  In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science 85, pp.77-91, March, 2012.
  [pdf (Full version with proofs and bug fixes)]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  On Bounding Problems of Quantitative Information Flow. (Extended Version)
  Journal of Computer Security 19 (6): pp.1029-1082 (2011).
  [pdf]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  On Bounding Problems of Quantitative Information Flow.
  In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science 6345, pp.357-372, Springer, September, 2010.
  [pdf (Full version with proofs)]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  Quantitative Information Flow - Verification Hardness and Possibilities.
  In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp.15-27, IEEE Computer Society, July, 2010.
  [pdf (Full version with proofs)]
  


• Tachio Terauchi.
  Dependent Types from Counterexamples.
  In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), ACM SIGPLAN Notices 45 (1), pp.119-130, ACM, January, 2010.
  [pdf (Full version with proofs and bug fixes), benchmarks]
  


• Hirotoshi Yasuoka and Tachio Terauchi.
  Polymorphic Fractional Capabilities.
  In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science 5673, pp.36-51, Springer, August, 2009.
  


• Tachio Terauchi.
  A Type System for Observational Determinism.
  In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp.287-300, IEEE Computer Society, June, 2008.
  [pdf (With bug fixes)]
  


• Tachio Terauchi.
  Checking Race Freedom via Linear Programming.
  In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), ACM SIGPLAN Notices 43 (6), pp.1-10, ACM, June, 2008.
  [pdf (With minor bug fixes)]
  


• Tachio Terauchi and Alex Aiken.
  A Capability Calculus for Concurrency and Determinism. (Extended Version)
  ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5): pp.27:1-27:30 (2008).
  [pdf]
  


• Tachio Terauchi and Alex Aiken.
  Witnessing Side Effects. (Extended Version)
  ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (3): pp.15:1-15:42 (2008).
  [pdf]
  


• Tachio Terauchi and Adam Megacz.
  Inferring Channel Buffer Bounds via Linear Programming.
  In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science 4960, pp.284-298, Springer, March, 2008.
  [pdf]
  


• Tachio Terauchi and Alex Aiken.
  A Capability Calculus for Concurrency and Determinism.
  In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR 2006), Lecture Notes in Computer Science 4137, pp.218-232, Springer, August, 2006.
  [pdf (Full version with proofs)]
  


• Tachio Terauchi and Alex Aiken.
  On Typability for Rank-2 Intersection Types with Polymorphic Recursion.
  In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006), pp.111-122, IEEE Computer Society, August, 2006.
  [pdf (Full version with proofs and fixes), Notes on Section 6]
  


• Tachio Terauchi and Alex Aiken.
  Witnessing Side-Effects.
  In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), ACM SIGPLAN Notices 40 (9), pp.105-115, ACM, September, 2005.
  [pdf]
  
  
• Tachio Terauchi and Alex Aiken.
  Secure Information Flow as a Safety Problem.
  In Proceedings of the 12th International Static Analysis Symposium (SAS 2005), Lecture Notes in Computer Science 3672, pp.352-367, Springer, September, 2005.
  [pdf (Full version with proofs and fixes)]
  


• Tachio Terauchi and Alex Aiken.
  Memory Management with Use-Counted Regions.
  Technical Report UCB//CSD-04-1314, University of California, Berkeley, March, 2004.
  [pdf]
  


• Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi.
  Checking and Inferring Local Non-Aliasing.
  In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), ACM SIGPLAN Notices 38 (5), pp.129-140, ACM, June, 2003.
  


• Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken.
  Flow-Sensitive Type Qualifiers.
  In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), ACM SIGPLAN Notices 37 (5), pp.1-12, ACM, June, 2002.
  


• Jinsong Cai, Aynur Dayanik, Hong Yu, Naveed Hasan, Tachio Terauchi, and William N. Grundy.
  Classification of Cancer Tissue Types by Support Vector Machines Using Micro Array Gene Expression Data. (Poster Presentation)
  In the 8th International Conference on Intelligent Systems for Molecular Biology (ISMB 2000), August, 2000.
  


• Tobias Höllerer, Steven Feiner, Tachio Terauchi, Gus Rashid, and Drexel Hallaway.
  Exploring MARS: Developing Indoor and Outdoor User Interfaces to a Mobile Augmented Reality System.
  Computers & Graphics 23 (6): (1999).