[Japanese Version]

Tachio Terauchi

Professor
Department of Computer Science and Engineering, Waseda University
(+81)-3-5286-3198
terauchi AT waseda DOT jp
[Researchmap.jp, Waseda University Researchers Database]

Bio

Tachio Terauchi is a professor in the Department of Computer Science and Engineering at Waseda University. He received his M.S. and Ph.D. from University of California, Berkeley in 2004 and 2006, and B.S. from Columbia University in 2000, all in computer science. Before joining Waseda, he was a professor at JAIST from 2014 to 2017, an associate professor at Nagoya University from 2011 to 2014, and an assistant professor at Tohoku University from 2007 to 2011. Terauchi is interested in techniques for building reliable computational systems. His work draws from, and contributes to the areas of programming languages, program verification and synthesis, mathematical logic and automated deduction, formal languages and automata theory, security, and type systems.

Teaching

• Design and Implementation of Programming Languages (Fall Semester)

Information for Prospective Students

• Information for Prospective Students (in Japanese)
• Laboratory introduction slides (in Japanese)
• Undergraduate research projects description
• Lab visits for 2024 will be appointment basis. Please send me an email to make an appointment.
• Lab visits will be at room 209B of Building 62W (or online, if preferred).

Professional Activities

• OOPSLA 2025 : Program Committee
• CSF 2025 : Program Committee
• PPL 2025 (Japanese) : Program Committee
• POPL 2025 : Program Committee
• ATVA 2024 : Program Committee
• FMCAD 2024 : Program Committee
• PLDI 2024 : Program Committee
• FSCD 2024 : Program Committee
• FLOPS 2024 : Program Committee
• CSF 2024 : Program Committee
• NII Shonan Meeting 180 : Co-Organizer
• APLAS 2023 : SRC & Posters Selection Committee
• ATVA 2023 : Program Committee
• ICCQ 2023 : Program Committee
• CSF 2023 : Program Committee
• ESOP 2023 : Program Committee
• OOPSLA 2022 : Program Committee
• PLDI 2022 : Program Committee
• CSF 2022 : Program Committee
• LICS 2022 : Program Committee
• POPL 2022 : Program Committee
• TMPA 2021 : Program Committee
• APLAS 2021 : Program Committee
• ATVA 2021 : Program Committee
• CAV 2021 : Program Committee
• CSF 2021 : Program Committee
• VSTTE 2020 : Program Committee
• ATVA 2020 : Program Committee
• FLOPS 2020 : Program Committee
• PPL 2020 (Japanese) : Program Committee
• TMPA 2019 : Program Committee
• APLAS 2019 : Program Committee
• ATVA 2019 : Program Committee
• SAS 2019 : Program Committee
• VSTTE 2019 : Program Committee
• APLAS 2018 : Program Committee
• VSTTE 2018 : Program Committee
• NII Shonan Meeting 115 : Co-Organizer
• POPL 2018 : Program Committee
• VMCAI 2018 : Program Committee
• APLAS 2017 : Program Committee
• RP 2017 : Program Committee
• VSTTE 2017 : Program Committee
• ESOP 2017 : Program Committee
• TMPA 2017 : Program Committee
• POPL 2017 : External Review Committee
• APLAS 2016 : Program Committee
• ICALP 2016 : Program Committee
• VMCAI 2016 : Program Committee
• POPL 2016 : External Review Committee
• NII Shonan Meeting 069 : Co-Organizer
• HOPA 2015 : Program Committee
• PLAS 2015 : Program Committee
• LICS 2015 : Program Committee
• FCS-FCC 2014 : Program Committee
• HOPA 2014 : Program Committee
• FLOPS 2014 : Program Committee
• VMCAI 2014 : Program Committee
• CSL 2013 : Program Committee
• POPL 2013 : External Review Committee
• APLAS 2012 : Program Committee
• POPL 2012 : Program Committee
• TLCA 2011 : Program Committee
• ESOP 2011 : Program Committee
• PLPV 2011 : Program Committee
• VMCAI 2011 : Program Committee
• TLDI 2011 : Program Committee
• PLDI 2010 : External Review Committee
• PPL 2010 (Japanese) : Program Co-Chair
• PLAS 2009 : Program Committee
• PPL 2009 (Japanese) : Program Committee
• SAC 2009 : Program Committee
• SAS 2008 : Program Committee

Students

• Nariyoshi Chida (Visiting Scholar)
• Tianrui Chen (D2)
• Taisei Nogami (D1)
• Ryunosuke Endo (M2)
• Koichiro Tomiie (M2)
• Toshiki Yamada (M2)
• Kazuma Kawahara (M2)
• Yuta Uchijo (M1)
• Naoya Anada (M1)
• Kaito Kimura (B4)
• Yuki Nakayama (B4)
• Taisei Iida (B4)
• Riru Oda (B3)

Publications [Google Scholar, Semantic Scholar, DBLP]

• Nariyoshi Chida and Tachio Terauchi.
  Repairing Regex-Dependent String Functions.
  In Proceedings of the 39th IEEE/ACM Interntional Conference on Automated Software Engineering (ASE 2024). To appear.
  [pdf]
  


• 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).
  


• Fuga Kawamata and Tachio Terauchi.
  Trace Effects for a Language with Algebraic Effect Handlers. (in Japanese)
  JSSST Computer Software 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.
  JSSST Computer Software 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)]
  


• Takuya Iwatsuka, Tachio Terauchi, and Shoji Yuen.
  Toward Verification of Hybrid System with Infinitesimal and Quantifier Elimination. (in Japanese)
  IPSJ Transactions on Programming 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).