TOP Page >  Profile

¾ðÊ󸦵æÅïIS Building £É£É¡¡6F
To Lab's Site


Full text / JAIST Repository



Tachio Terauchi Professor
School of Information Science¡¢Intelligent Robotics Area


B.S. from Columbia University (2000), M.S. from University of California at Berkeley (2004), Ph.D from University of California at Berkeley (2006)

¢£Professional Career

Assistant Professor at Tohoku University (2007), Associate Professor at Nagoya University (2011), Professor at Japan Advanced Institute of Science and Technology (2014)


Program Analysis and Program Verification

¢£Research Keywords

Programming Languages, Type Systems, Software Model Checking, Automated Deduction, Computer Security

¢£Research Interests

Please see the lab web page


¡þPublished Papers

  • Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels¡¤Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei¡¤In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), pp. 362-375, ACM, June, 2017
  • Compositional Synthesis of Leakage Resilient Programs¡¤Arthur Blot, Masaki Yamamoto, and Tachio Terauchi¡¤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.
  • Temporal Verification of Higher-Order Functional Programs¡¤Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno¡¤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

Display All

¡þLectures and Presentations

  • Predicate Refinement Heuristics in Program Verification with CEGAR (Invited Talk)¡¤Tachio Terauchi¡¤The 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016)¡¤Eindhoven, Netherlands¡¤April, 2016
  • Temporal Verification of Higher-Order Functional Programs¡¤Tachio Terauchi¡¤Dagstuhl Seminar 16131: Language Based Verification Tools for Functional Programs¡¤Dagstuhl, Germany¡¤March, 2016
  • Temporal Verification of Higher-Order Functional Programs¡¤Tachio Terauchi¡¤NII Shonan Meeting Seminar 078: Higher-Order Model Checking¡¤Hayamamachi, Japan¡¤March, 2016

Display All

¢£Extramural Activities

¡þAcademic Society Affiliations

  • ACM¡¤Member¡¤2014-
  • Information Processing Society in Japan¡¤Member¡¤2009-

¡þOther Activities

  • The 4th International Conference on Tools and Methods of Program Analsyis (TMPA 2017)¡¤Program Commitee
  • The 26th European Symposium on Programming (ESOP 2017)¡¤Program Committee
  • The 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)¡¤Program Committee

Display All

¢£Academic Awards Received

  • Graduate Assistance in Areas of National Need Fellowship¡¤U.S. Department of Education¡¤2000