| 2026 | CAV | Repairing Regex-Dependent String-Manipulation Programs. | Nariyoshi Chida, Tachio Terauchi |
| 2025 | APLAS | Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers. | Ryunosuke Endo, Tachio Terauchi |
| 2025 | MFCS | Efficient Matching of Some Fundamental Regular Expressions with Backreferences. | Taisei Nogami, Tachio Terauchi |
| 2023 | MFCS | On the Expressive Power of Regular Expressions with Backreferences. | Taisei Nogami, Tachio Terauchi |
| 2022 | FSCD | On Lookaheads in Regular Expressions with Backreferences. | Nariyoshi Chida, Tachio Terauchi |
| 2022 | SP | Repairing DoS Vulnerability of Real-World Regexes. | Nariyoshi Chida, Tachio Terauchi |
| 2021 | CAV | Constraint-Based Relational Verification. | Hiroshi Unno, Tachio Terauchi, Eric Koskinen |
| 2018 | LICS | A Fixpoint Logic and Dependent Effects for Temporal Property Verification. | Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi |
| 2017 | PLDI | Decomposition instead of self-composition for proving the absence of timing channels. | Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei |
| 2016 | POPL | Temporal verification of higher-order functional programs. | Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno |
| 2015 | ESOP | Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. | Tachio Terauchi, Hiroshi Unno |
| 2015 | SAS | Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR. | Tachio Terauchi |
| 2015 | TACAS | Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. | Hiroshi Unno, Tachio Terauchi |
| 2014 | CSL | Local temporal reasoning. | Eric Koskinen, Tachio Terauchi |
| 2014 | ESOP | Automatic Termination Verification for Higher-Order Functional Programs. | Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi |
| 2013 | POPL | Automating relatively complete verification of higher-order functional programs. | Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi |
| 2012 | FLOPS | Automated Verification of Higher-Order Functional Programs. | Tachio Terauchi |
| 2010 | ESORICS | On Bounding Problems of Quantitative Information Flow. | Hirotoshi Yasuoka, Tachio Terauchi |
| 2010 | POPL | Dependent types from counterexamples. | Tachio Terauchi |
| 2009 | SAS | Polymorphic Fractional Capabilities. | Hirotoshi Yasuoka, Tachio Terauchi |
| 2008 | ESOP | Inferring Channel Buffer Bounds Via Linear Programming. | Tachio Terauchi, Adam Megacz |
| 2008 | PLDI | Checking race freedom via linear programming. | Tachio Terauchi |
| 2006 | CONCUR | A Capability Calculus for Concurrency and Determinism. | Tachio Terauchi, Alex Aiken |
| 2006 | LICS | On Typability for Rank-2 Intersection Types with Polymorphic Recursion. | Tachio Terauchi, Alex Aiken |
| 2005 | ICFP | Witnessing side-effects. | Tachio Terauchi, Alex Aiken |
| 2005 | SAS | Secure Information Flow as a Safety Problem. | Tachio Terauchi, Alex Aiken |
| 2003 | PLDI | Checking and inferring local non-aliasing. | Alex Aiken, Jeffrey S. Foster, John Kodumal, Tachio Terauchi |
| 2002 | PLDI | Flow-Sensitive Type Qualifiers. | Jeffrey S. Foster, Tachio Terauchi, Alex Aiken |