Exploring MARS: developing indoor and outdoor user interfaces to a mobile augmented reality system. - Tobias Höllerer; Steven Feiner; Tachio Terauchi; Gus Rashid; Drexel Hallaway (Comput. Graph., 1999)

Flow-Sensitive Type Qualifiers. - Jeffrey S. Foster; Tachio Terauchi; Alex Aiken (PLDI, 2002)

Checking and inferring local non-aliasing. - Alex Aiken; Jeffrey S. Foster; John Kodumal; Tachio Terauchi (PLDI, 2003)

Secure Information Flow as a Safety Problem. - Tachio Terauchi; Alex Aiken (SAS, 2005)

On Typability for Rank-2 Intersection Types with Polymorphic Recursion. - Tachio Terauchi; Alex Aiken (LICS, 2006)

A Type System for Observational Determinism. - Tachio Terauchi (CSF, 2008)

Inferring Channel Buffer Bounds Via Linear Programming. - Tachio Terauchi; Adam Megacz (ESOP, 2008)

Checking race freedom via linear programming. - Tachio Terauchi (PLDI, 2008)

Witnessing side effects. - Tachio Terauchi; Alex Aiken (ACM Trans. Program. Lang. Syst., 2008)

A capability calculus for concurrency and determinism. - Tachio Terauchi; Alex Aiken (ACM Trans. Program. Lang. Syst., 2008)

Polymorphic Fractional Capabilities. - Hirotoshi Yasuoka; Tachio Terauchi (SAS, 2009)

Quantitative Information Flow - Verification Hardness and Possibilities. - Hirotoshi Yasuoka; Tachio Terauchi (CSF, 2010)

Dependent types from counterexamples. - Tachio Terauchi (POPL, 2010)

On bounding problems of quantitative information flow. - Hirotoshi Yasuoka; Tachio Terauchi (J. Comput. Secur., 2011)

Automated Verification of Higher-Order Functional Programs. - Tachio Terauchi (FLOPS, 2012)

Automating relatively complete verification of higher-order functional programs. - Hiroshi Unno 001; Tachio Terauchi; Naoki Kobayashi 001 (POPL, 2013)

Local temporal reasoning. - Eric Koskinen; Tachio Terauchi (CSL-LICS, 2014)

Automatic Termination Verification for Higher-Order Functional Programs. - Takuya Kuwahara; Tachio Terauchi; Hiroshi Unno 001; Naoki Kobayashi 001 (ESOP, 2014)

Quantitative information flow as safety and liveness hyperproperties. - Hirotoshi Yasuoka; Tachio Terauchi (Theor. Comput. Sci., 2014)

Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. - Tachio Terauchi; Hiroshi Unno 001 (ESOP, 2015)

Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR. - Tachio Terauchi (SAS, 2015)

Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. - Hiroshi Unno 001; Tachio Terauchi (TACAS, 2015)

Logic and Verification Methods in Security and Privacy (NII Shonan Meeting 2015-16). - Marco Gaboardi; Vivek Nigam; Tachio Terauchi (NII Shonan Meet. Rep., 2015)

Temporal verification of higher-order functional programs. - Akihiro Murase; Tachio Terauchi; Naoki Kobayashi 001; Ryosuke Sato 001; Hiroshi Unno 001 (POPL, 2016)

Decomposition instead of self-composition for proving the absence of timing channels. - Timos Antonopoulos; Paul Gazzillo; Michael Hicks 001; Eric Koskinen; Tachio Terauchi; Shiyi Wei (PLDI, 2017)

Compositional Synthesis of Leakage Resilient Programs. - Arthur Blot; Masaki Yamamoto 004; Tachio Terauchi (POST, 2017)

A Fixpoint Logic and Dependent Effects for Temporal Property Verification. - Yoji Nanjo; Hiroshi Unno 001; Eric Koskinen; Tachio Terauchi (LICS, 2018)

Relatively complete refinement type system for verification of higher-order non-deterministic programs. - Hiroshi Unno 001; Yuki Satake; Tachio Terauchi (Proc. ACM Program. Lang., 2018)

Intensional and extensional aspects of computation: From computability and complexity to program analysis and security (NII Shonan Meeting 2018-1). - Roberto Giacobazzi; Dusko Pavlovic; Tachio Terauchi (NII Shonan Meet. Rep., 2018)

Games for Security Under Adaptive Adversaries. - Timos Antonopoulos; Tachio Terauchi (CSF, 2019)

A Formal Analysis of Timing Channel Security via Bucketing. - Tachio Terauchi; Timos Antonopoulos (POST, 2019)

Program Verification via Predicate Constraint Satisfiability Modulo Theories. - Hiroshi Unno 001; Yuki Satake; Tachio Terauchi; Eric Koskinen (CoRR, 2020)

Automatic Repair of Vulnerable Regular Expressions. - Nariyoshi Chida; Tachio Terauchi (CoRR, 2020)

Bucketing and information flow analysis for provable timing attack mitigation. - Tachio Terauchi; Timos Antonopoulos (J. Comput. Secur., 2020)

Constraint-Based Relational Verification. - Hiroshi Unno 001; Tachio Terauchi; Eric Koskinen (CAV (1), 2021)

Repairing DoS Vulnerability of Real-World Regexes. - Nariyoshi Chida; Tachio Terauchi (SP, 2022)

On the Expressive Power of Regular Expressions with Backreferences. - Taisei Nogami; Tachio Terauchi (MFCS, 2023)

Repairing Regular Expressions for Extraction. - Nariyoshi Chida; Tachio Terauchi (Proc. ACM Program. Lang., 2023)

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. - Hiroshi Unno 001; Tachio Terauchi; Yu Gu 022; Eric Koskinen (Proc. ACM Program. Lang., 2023)

On Lookaheads in Regular Expressions with Backreferences. - Nariyoshi Chida; Tachio Terauchi (IEICE Trans. Inf. Syst., 2023)

Repairing Regex-Dependent String Functions. - Nariyoshi Chida; Tachio Terauchi (ASE, 2024)

Regular Expressions with Backreferences on Multiple Context-Free Languages, and the Closed-Star Condition. - Taisei Nogami; Tachio Terauchi (CoRR, 2024)

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. - Fuga Kawamata; Hiroshi Unno 001; Taro Sekiyama; Tachio Terauchi (Proc. ACM Program. Lang., 2024)

On DoS Vulnerability of Regular Expressions, with and Without Backreferences. - Tachio Terauchi (CSF, 2025)

Efficient Matching of Some Fundamental Regular Expressions with Backreferences. - Taisei Nogami; Tachio Terauchi (MFCS, 2025)

Measuring the expressive power of practical regular expressions by classical stacking automata models. - Taisei Nogami; Tachio Terauchi (Inf. Comput., 2025)

Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers. - Ryunosuke Endo; Tachio Terauchi (CoRR, 2025)