[Japanese Version]
Tachio Terauchi
Professor
Department of Computer Science and Engineering, Waseda University
(+81)352863198
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
Professional Activities
Show more
Show less
Students
 Nariyoshi Chida (Visiting Scholar)
 Tianrui Chen (D1)
 Fuga Kawamata (M2)
 Ryunosuke Endo (M1)
 Koichiro Tomiie (M1)
 Taisei Nogami (M1)
 Toshiki Yamada (M1)
 Kazuma Kawahara (M1)
 Yuta Uchijo (M0)
 Naoya Anada (M0)
 Kaito Kimura (B3)
 Tomoya Aoyagi (B3)
Past Students

Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi.
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.
In Proceedings of the 51st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2024), To Appear.
[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:171:15, Schloss Dagstuhl LeibnizZentrum für Informatik, August, 2023.
[pdf (Full version with appendices)]

Nariyoshi Chida and Tachio Terauchi.
Reparing Regular Expressions for Extraction.
In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), PACMPL 7(PLDI): pp.16331656, 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 E106D (5), pp.959975, (2023).

Fuga Kawamata and Tachio Terauchi.
Trace Effects for a Language with Algebraic Effect Handlers. (in Japanese)
JSSST Computer Software 40 (2), pp.1948, (2023).

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen.
Modular PrimalDual Fixpoint Logic Solving for Temporal Verification.
In Proceedings of the 50th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2023), PACMPL 7(POPL): pp.21112140, 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:115:18, Schloss Dagstuhl LeibnizZentrum für Informatik, August, 2022.
[pdf]

Nariyoshi Chida and Tachio Terauchi.
Repairing DoS Vulnerability of RealWorld Regexes.
In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), IEEE Computer Society, pp.20602077, 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.
Constraintbased Relational Verification.
In Proceedings of the 33rd International Conference on ComputerAided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742766, 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.607634 (2020).
[pdf]

Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno.
Failure of CutElimination in Cyclic Proofs of Separation Logic.
JSSST Computer Software 37 (1), pp.3952, (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.216229, 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.2950, 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.759768, ACM, July, 2018.
[pdf]

Hiroshi Unno, Yuki Satake, and Tachio Terauchi.
Relatively Complete Refinement Type System for Verification of HigherOrder Nondeterministic Programs.
In Proceedings of the 45th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2018), PACMPL 2(POPL): pp.12:112:29. ACM, January, 2018.
[pdf]

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei.
Decomposition Instead of SelfComposition 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.362375, 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.277297, Springer, April, 2017.
[pdf (Full version with proofs)]

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno.
Temporal Verification of HigherOrder Functional Programs.
In Proceedings of the 43rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices 51 (1), pp.5768, 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.128144, Springer, September, 2015.
[pdf (Full version with proofs)]

Hiroshi Unno and Tachio Terauchi.
Inferring Simple Solutions to Recursionfree 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.149163, 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.610633, 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 (CSLLICS 2014), pp.59:159: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.167182 (2014).
 Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi.
Automatic Termination Verification for HigherOrder Functional Programs.
In Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 8410, pp.392411, 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.2032 (2013).
 Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi.
Automating Relatively Complete Verification of HigherOrder Functional Programs.
In Proceedings of the 40th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2013), ACM SIGPLAN Notices 48 (1), pp.7586, 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.7791, 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.10291082 (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.357372, 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.1527, IEEE Computer Society, July, 2010.
[pdf (Full version with proofs)]
 Tachio Terauchi.
Dependent Types from Counterexamples.
In Proceedings of the 37th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2010), ACM SIGPLAN Notices 45 (1), pp.119130, 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.3651, Springer, August, 2009.

Tachio Terauchi.
A Type System for Observational Determinism.
In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp.287300, 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.110, 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:127: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:115: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.284298, 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.218232, Springer, August, 2006.
[pdf (Full version with proofs)]

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

Tachio Terauchi and Alex Aiken.
Witnessing SideEffects.
In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), ACM SIGPLAN Notices 40 (9), pp.105115, 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.352367, Springer, September, 2005.
[pdf (Full version with proofs and fixes)]

Tachio Terauchi and Alex Aiken.
Memory Management with UseCounted Regions.
Technical Report UCB//CSD041314, University of California, Berkeley, March, 2004.
[pdf]

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

Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken.
FlowSensitive Type Qualifiers.
In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), ACM SIGPLAN Notices 37 (5), pp.112, 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).