TERAUCHI, Tachio

写真a

Affiliation

Faculty of Science and Engineering, School of Fundamental Science and Engineering

Job title

Professor

Homepage URL

http://www.f.waseda.jp/terauchi/

Profile

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 analysis, program verification, program synthesis, type systems, mathematical logic, automated deduction, and security.

Research Institute 【 display / non-display

  • 2020
    -
    2022

    理工学術院総合研究所   兼任研究員

Education 【 display / non-display

  • 2000.09
    -
    2006.08

    University of California, Berkeley   Department of Electrical Engineering and Computer Sciences   Computer Science Division  

  • 1996.09
    -
    2000.05

    Columbia University   School of Engineering and Applied Science   Computer Science Major  

Degree 【 display / non-display

  • University of California, Berkeley   Ph.D.

  • University of California, Berkeley   M.S.

  • Columbia University   B.S.

Research Experience 【 display / non-display

  • 2017.09
    -
    Now

    Waseda University   Department of Computer Science and Engineering   Professor

  • 2014.04
    -
    2017.09

    Japan Advanced Institute of Science and Technology   School of Information Science   Professor

  • 2011.04
    -
    2014.03

    Nagoya University   Graduate School of Information Science   Associate professor

  • 2007.01
    -
    2011.03

    Tohoku University   Graduate School of Information Sciences   Assistant Professor

Professional Memberships 【 display / non-display

  •  
     
     

    ACM

  •  
     
     

    INFORMATION PROCESSING SOCIETY OF JAPAN

  •  
     
     

    Japan Society for Software Science and Technology

 

Research Areas 【 display / non-display

  • Theory of informatics

  • Software

Research Interests 【 display / non-display

  • Programming Languages

  • Program Verification

  • Program Synthesis

  • Type Systems

  • Automated Deduction

display all >>

Papers 【 display / non-display

  • Constraint-based Relational Verification

    Hiroshi Unno, Tachio Terauchi, Eric Koskinen

    In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759, pp.742-766, Springer    2021  [Refereed]

  • Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation

    Tachio Terauchi, Timos Antonopoulos

    Journal of Computer Security   28 ( 6 ) 607 - 634  2020  [Refereed]  [International journal]  [International coauthorship]

    DOI

  • Failure of Cut-Elimination in Cyclic Proofs of Separation Logic

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

    Computer Software   37 ( 1 ) 1_39 - 1_52  2020  [Refereed]  [Invited]  [Domestic journal]

     View Summary

    <p>This paper studies the role of the cut rule in cyclic proof systems for separation logic. A cyclic proof system is a sequent-calculus style proof system for proving properties involving inductively defined predicates. Recently, there has been much interest in using cyclic proofs for proving properties described in separation logic with inductively defined predicates. In particular, for program verification, several theorem provers based on mechanical proof search procedures in cyclic proof systems for separation logic have been proposed. This paper shows that the cut-elimination property fails in cyclic proof systems for separation logic in several settings. We present two systems, one for sequents with single-antecedent and single-conclusion, and another for sequents with single-antecedent and multiple-conclusions. To show the cut-elimination failure, we present concrete and reasonably simple counter-example sequents which the systems can prove with cuts but not without cuts. This result suggests that the cut rule is important for a practical application of cyclic proofs to separation logic, since a naïve proof search procedure, which tries to find a cut-free proof, gives a limit to what one would be able to prove.</p>

    DOI CiNii

  • Games for Security under Adaptive Adversaries.

    Timos Antonopoulos, Tachio Terauchi

    In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019), pp.216-229, IEEE Computer Society    2019  [Refereed]  [International journal]

    DOI

  • A Formal Analysis of Timing Channel Security via Bucketing.

    Tachio Terauchi, Timos Antonopoulos

    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    2019  [Refereed]  [International journal]

    DOI

display all >>

Awards 【 display / non-display

  • WASEDA RESEARCH AWARD High-Impact Publication

    2019.12   Waseda University  

    Winner: Tachio Terauchi

  • The EASST Award for the Best ETAPS Paper Related to the Systematic and Rigorous Engineering of Software and Systems.

    2017.04   European Association for Software Science and Technology   Nominee

    Winner: Arthur Blot, Masaki Yamamoto, Tachio Terauchi

  • 発表賞(一般)

    2008.03   ソフトウェア科学会 第10回プログラミングおよびプログラミング言語ワークショップ (PPL 2008)  

    Winner: 寺内 多智弘

  • 第4回野口研究奨励賞

    2008   情報処理学会 東北支部  

    Winner: 寺内 多智弘

Research Projects 【 display / non-display

  • Understanding malware semantics by AI-supported formal methods

    Challenging Research (Pioneering)

    Project Year :

    2020.07
    -
    2026.03
     

  • Synthesis of High-Level Programs from Temporal and Relational Specifications

    Grant-in-Aid for Scientific Research (B)

    Project Year :

    2020.04
    -
    2025.03
     

  • Verification of high-level programs containing mutable higher-order recursive data structures

    Grant-in-Aid for Scientific Research (B)

    Project Year :

    2017.04
    -
    2022.03
     

    Tachio Terauchi, Hiroshi Unno

  • Program verification and program synthesis for side-channel attack resilience

    Challenging Research (Exploratory)

    Project Year :

    2018.06
    -
    2021.03
     

    Tachio Terauchi

  • Foundation of a Global Core Research Center for Mathematical Logic and its Application.

    Project Year :

    2015.04
    -
    2020.03
     

    Hajime Ishihara

display all >>

Presentations 【 display / non-display

  • Constraint-based Relational Verification

    Tachio Terauchi  [Invited]

    Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021) 

    Presentation date: 2021.10

  • Inferring Simple Strategies for Efficient Quantified SMT Solving (Poster Presentation)

    Souta Yamauchi, Tachio Terauchi

    17th Asian Symposium on Programming Languages and Systems (APLAS 2019) 

    Presentation date: 2019.12

  • A Fixpoint Logic and Dependent Effects for Temporal Property Verification

    Tachio Terauchi  [Invited]

    Dagstuhl Seminar 19371: Deduction Beyond Satisfiability 

    Presentation date: 2019.09

  • Solving First-Order Fixpoint Logic for Program Verification

    Tachio Terauchi  [Invited]

    Third Workshop on Mathematical Logic and its Applications (MLA 2019) 

    Presentation date: 2019.03

  • On Cut-Elimination Theorem in Cyclic-Proof Systems

    Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome

    Third Workshop on Mathematical Logic and its Applications (MLA 2019) 

    Presentation date: 2019.03

display all >>

 

Syllabus 【 display / non-display

display all >>

 

Committee Memberships 【 display / non-display

  • 2020.04
    -
    Now

    JSSST Special Interest Group on Programming and Programming Languages  Steering Committee

  • 2018.04
    -
    Now

    IPSJ Special Interest Group on Programming  Steering Committee

  • 2021
    -
    2022

    The 37th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2022)  Program Committee

  • 2021
    -
    2022

    The 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022)  Program Committee

  • 2021
    -
    2022

    The 35th IEEE Computer Security Foundations Symposium (CSF 2022)  Program Committee

display all >>