Updated on 2022/11/26

写真a

 
TERAUCHI, Tachio
 
Scopus Paper Info  
Paper Count: 0  Citation Count: 0  h-index: 9

Citation count denotes the number of citations in papers published for a particular year.

Affiliation
Faculty of Science and Engineering, School of Fundamental Science and Engineering
Job title
Professor
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

  • 2020
    -
    2022

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

Education

  • 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

  • University of California, Berkeley   Ph.D.

  • University of California, Berkeley   M.S.

  • Columbia University   B.S.

Research Experience

  • 2017.10
    -
    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

  •  
     
     

    ACM

  •  
     
     

    INFORMATION PROCESSING SOCIETY OF JAPAN

  •  
     
     

    Japan Society for Software Science and Technology

 

Research Areas

  • Software

  • Theory of informatics

Research Interests

  • Programming Languages

  • Program Verification

  • Program Synthesis

  • Type Systems

  • Automated Deduction

  • Security

▼display all

Papers

  • On Lookaheads in Regular Expressions with Backreferences

    Nariyoshi Chida, Tachio Terauchi

    In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp.15:1-15:18, Schloss Dagstuhl Leibniz-Zentrum für Informatik    2022  [Refereed]

    DOI

    Scopus

  • Repairing DoS Vulnerability of Real-World Regexes

    Nariyoshi Chida, Tachio Terauchi

    In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), pp.2060-2077, IEEE Computer Society    2022  [Refereed]

    DOI

    Scopus

  • 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]

    DOI

    Scopus

    2
    Citation
    (Scopus)
  • 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

    Scopus

  • 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

    Scopus

    5
    Citation
    (Scopus)
  • 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

    Scopus

    1
    Citation
    (Scopus)
  • 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

    Scopus

    2
    Citation
    (Scopus)
  • A Fixpoint Logic and Dependent Effects for Temporal Property Verification.

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

    In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pp. 759-768, ACM    2018  [Refereed]  [International journal]

    DOI

    Scopus

    9
    Citation
    (Scopus)
  • Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs.

    Hiroshi Unno, Yuki Satake, Tachio Terauchi

    PACMPL   2 ( POPL ) 12:1-12:29  2018  [Refereed]  [International journal]

    DOI

    Scopus

    8
    Citation
    (Scopus)
  • Compositional synthesis of leakage resilient programs

    Arthur Blot, Masaki Yamamoto, 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    2017  [Refereed]  [International journal]

     View Summary

    A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal sense. One such formal notion of leakage resilience is the n-threshold-probing model proposed in the seminal work by Ishai et al. [16]. In a recent work [9], Eldib and Wang have proposed a method for automatically synthesizing programs that are leakage resilient according to this model, for the case n = 1. In this paper, we show that the n-threshold-probing model of leakage resilience enjoys a certain compositionality property that can be exploited for synthesis.We use the property to design a synthesis method that efficiently synthesizes leakage-resilient programs in a compositional manner, for the general case of n &gt
    1. We have implemented a prototype of the synthesis algorithm, and we demonstrate its effectiveness by synthesizing leakage-resilient versions of benchmarks taken from the literature.

    DOI

    Scopus

    7
    Citation
    (Scopus)
  • Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels

    Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei

    In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices 52 (6), pp.362-375. ACM    2017  [Refereed]  [International journal]

     View Summary

    We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (k &gt;= 2) executions at once.
    We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demand-driven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems.

    DOI

    Scopus

    9
    Citation
    (Scopus)
  • Temporal verification of higher-order functional programs

    Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, 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.    2016  [Refereed]

     View Summary

    We present an automated approach to verifying arbitrary omega regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

    DOI

    Scopus

    9
    Citation
    (Scopus)
  • Inferring simple solutions to recursion-free horn clauses via sampling

    Hiroshi Unno, Tachio Terauchi

    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.149-163, Springer    2015  [Refereed]

     View Summary

    Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.

    DOI

    Scopus

    6
    Citation
    (Scopus)
  • Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi

    In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.128-144, Springer    2015  [Refereed]

     View Summary

    Safety property (i.e., reachability) verification is undecidable for Turing-complete programming languages. Nonetheless, recent progress has lead to heuristic verification methods, such as the ones based on predicate abstraction with counter example-guided refinement (CEGAR), that work surprisingly well in practice. In this paper, we investigate the effectiveness of the small refinement heuristic which, for abstraction refinement in CEGAR, uses (the predicates in) a small proof of the given counterexample's spuriousness [3,12,17,22]. Such a method has shown to be quite effective in practice but thus far lacked a theoretical backing. Our core result is that the heuristic guarantees certain bounds on the number of CEGAR iterations, relative to the size of a proof for the input program.

    DOI

    Scopus

    1
    Citation
    (Scopus)
  • Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement

    Tachio Terauchi, Hiroshi Unno

    In Proceedings of the 24th European Symposium on Programming (ESOP 2015), Lecture Notes in Computer Science 9032, pp.610-633, Springer    2015  [Refereed]

     View Summary

    In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it is guaranteed to eventually find predicates sufficient to prove the given property, when such exist. However, existing complete methods require deciding if a proof of the counterexample's spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs a heavy overhead. In this paper, we address the issue by showing that the language restriction can be relaxed so that the refinement process is restricted to infer proofs from some finite language L-base boolean OR L-ext but is only required to return a proof when the counterexample's spuriousness can be proved in L-base. Then, we show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and be complete by restricting only the theory-level reasoning in SMT to emit L-base-restricted partial interpolants (while such an approach has been proposed previously, we show for the first time that it can be done for languages that are not closed under conjunctions and disjunctions). We also present a technique that uses a property of counterexample patterns to further improve the efficiency of the refinement algorithm while still satisfying the requirement. We have experimented with a prototype implementation of the new refinement algorithm, and show that it is able to achieve complete refinement with only a small overhead.

    DOI

    Scopus

    2
    Citation
    (Scopus)
  • Automatic Termination Verification for Higher-Order Functional Programs

    Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

    In Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science 8410, pp.392-411, Springer    2014  [Refereed]

     View Summary

    We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.

    DOI

    Scopus

    25
    Citation
    (Scopus)
  • Local temporal reasoning

    Eric Koskinen, Tachio Terauchi

    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 (CSL-LICS 2014), pp.59:1-59:10, ACM    2014  [Refereed]

     View Summary

    We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs. Copyright © 2014 ACM.

    DOI

    Scopus

    15
    Citation
    (Scopus)
  • Quantitative information flow as safety and liveness hyperproperties

    Hirotoshi Yasuoka, Tachio Terauchi

    Theoretical Computer Science   538   167 - 182  2014  [Refereed]

     View Summary

    We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call "k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition. (C) 2013 Elsevier B.V. All rights reserved.

    DOI

    Scopus

    17
    Citation
    (Scopus)
  • Automating relatively complete verification of higher-order functional programs

    Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

    In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), ACM SIGPLAN Notices 48 (1), pp.75-86, ACM, January, 2013.    2013.01  [Refereed]

     View Summary

    We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs. Copyright © 2013 ACM.

    DOI

    Scopus

    11
    Citation
    (Scopus)
  • Toward Verification of Hybrid System with Infinitesimal and Quantifier Elimination

    Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

    IPSJ Transactions on Programming   6 ( 3 ) 20 - 32  2013  [Refereed]

    CiNii

  • Quantitative information flow as safety and liveness hyperproperties

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science 85, pp.77-91    2012  [Refereed]

     View Summary

    We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call "k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.

    DOI

    Scopus

    4
    Citation
    (Scopus)
  • On bounding problems of quantitative information flow

    Hirotoshi Yasuoka, Tachio Terauchi

    Journal of Computer Security   19 ( 6 ) 1029 - 1082  2011  [Refereed]  [Invited]

     View Summary

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow. © 2011 - IOS Press and the authors. All rights reserved.

    DOI

    Scopus

    15
    Citation
    (Scopus)
  • Dependent Types from Counterexamples

    Tachio Terauchi

    In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), ACM SIGPLAN Notices 45 (1), pp.119-130, ACM    2010  [Refereed]

     View Summary

    Motivated by recent research in abstract model checking, we present a new approach to inferring dependent types. Unlike many of the existing approaches, our approach does not rely on programmers to supply the candidate (or the correct) types for the recursive functions and instead does counterexample-guided refinement to automatically generate the set of candidate dependent types. The main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found untypable with the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real type error or generate additional candidate dependent types to refute the spurious counterexample. The process is repeated until either a real type error is found or sufficient candidates are generated to prove the program typable. Our system makes non-trivial use of "linear" intersection types in the refinement phase.
    The paper presents the type inference system and reports on the experience with a prototype implementation that infers dependent types for a subset of the Ocaml language. The implementation infers dependent types containing predicates from the quantifier-free theory of linear arithmetic and equality with uninterpreted function symbols.

    DOI

    Scopus

    12
    Citation
    (Scopus)
  • On Bounding Problems of Quantitative Information Flow

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science 6345, pp.357-372, Springer    2010  [Refereed]

     View Summary

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not; a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not; amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free boolean programs. Specifically, we show that the problem is PP-hard for all the definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

    DOI

    Scopus

    13
    Citation
    (Scopus)
  • Quantitative Information Flow - Verification Hardness and Possibilities

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp.15-27, IEEE Computer Society    2010  [Refereed]

     View Summary

    Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions.
    We prove that, even for just comparing two programs on which has the larger flow, none of the definitions is a k-safety property for any k, and therefore is not amenable to the self-composition technique that has been successfully applied to precisely checking non-interference. We also show a complexity theoretic gap with non-interference by proving that, for loop-free boolean programs whose non-interference is coNP-complete, the comparison problem is #P-hard for all of the definitions.
    For positive results, we show that universally quantifying the distribution in the comparison problem, that is, comparing two programs according to the entropy based definitions on which has the larger flow for all distributions, is a 2-safety problem in general and is coNP-complete when restricted for loop-free boolean programs. We prove this by showing that the problem is equivalent to a simple relation naturally expressing the fact that one program is more secure than the other. We prove that the relation also refines the channel-capacity based definition, and that it can be precisely checked via the self-composition as well as the "interleaved" self-composition technique.

    DOI

    Scopus

    41
    Citation
    (Scopus)
  • Polymorphic Fractional Capabilities

    Hirotoshi Yasuoka, Tachio Terauchi

    In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science 5673, pp.36-51, Springer.    2009  [Refereed]

     View Summary

    The capability calculus is a framework for statically reasoning about program resources such as deallocatable memory regions. Fractional capabilities, originally proposed by Boyland for checking the determinism of parallel reads hi multi-thread programs, extend the capability calculus by extending the capabilities to range over the rational numbers. Fractional capabilities have since found numerous applications, including race detection, buffer bound inference, security analyses, and separation logic. However, previous work on fractional capability systems either lacked polymorphism or lacked an efficient inference procedure. Automated inference is important; for the application of the calculus to static analysis. This paper addresses the issue by presenting a, polymorphic fractional capability calculus that, allows polynomial-time inference via a reduction to rational linear programming.

    DOI

    Scopus

    5
    Citation
    (Scopus)
  • Witnessing side effects

    Tachio Terauchi, Alex Aiken

    ACM Transactions on Programming Languages and Systems (TOPLAS)   30 ( 3 ) 15:1-15:42  2008.05  [Refereed]

     View Summary

    We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.

    DOI

    Scopus

    6
    Citation
    (Scopus)
  • A capability calculus for concurrency and determinism

    Tachio Terauchi, Alex Aiken

    ACM Transactions on Programming Languages and Systems (TOPLAS)   30 ( 5 ) 27:1 - 27:30  2008  [Refereed]

     View Summary

    This article presents a static system for checking determinism (technically, partial confluence) of communicating concurrent processes. Our approach automatically detects partial confluence in programs communicating via a mix of different kinds of communication methods: rendezvous channels, buffered channels, broadcast channels, and reference cells. Our system reduces the partial confluence checking problem in polynomial time (in the size of the program) to the problem of solving a system of rational linear inequalities, and is thus efficient.

    DOI

    Scopus

    22
    Citation
    (Scopus)
  • Checking race freedom via linear programming

    Tachio Terauchi

    In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), ACM SIGPLAN Notices 43 (6), pp.1-10, ACM    2008  [Refereed]

     View Summary

    We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to ( rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

    DOI

    Scopus

    4
    Citation
    (Scopus)
  • Inferring channel buffer bounds via linear programming

    Tachio Terauchi, Adam Megacz

    In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science 4960, pp.284-298, Springer    2008  [Refereed]

     View Summary

    We present a static analysis for inferring the maximum amount of buffer space used by a program consisting of concurrently running processes communicating via buffered channels. We reduce the problem to linear programming by casting the analysis as a fractional capability calculus system. Our analysis can reason about buffers used by multiple processes concurrently, and runs in time polynomial in the size of the program.

    DOI

    Scopus

    2
    Citation
    (Scopus)
  • A type system for observational determinism

    Tachio Terauchi

    In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp.287-300, IEEE Computer Society    2008  [Refereed]

     View Summary

    Zdancewic and Myers introduced observational determinism as a scheduler independent notion of security for concurrent programs. This paper proposes a type system for verifying observational determinism. Our type system verifies observational determinism by itself and does not require the type checked program to be confluent. A polynomial time type inference algorithm is also presented.

    DOI

    Scopus

    31
    Citation
    (Scopus)
  • On typability for rank-2 intersection types with polymorphic recursion

    Tachio Terauchi, Alex Aiken

    In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006), pp.111-122, IEEE Computer Society    2006  [Refereed]

     View Summary

    We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a conte-xtfree language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problemfor Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the MilnerMycroft type system. We also show undecidability of a related program analysis problem.

    DOI

    Scopus

    3
    Citation
    (Scopus)
  • A capability calculus for concurrency and determinism

    Tachio Terauchi, Alex Aiken

    In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR 2006), Lecture Notes in Computer Science 4137, pp.218-232, Springer    2006  [Refereed]

     View Summary

    We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent than previous approaches and is able to handle a mix of different kinds of communication channels, including shared reference cells.

    DOI

    Scopus

    10
    Citation
    (Scopus)
  • Secure information flow as a safety problem

    T Terauchi, A Aiken

    In Proceedings of the 12th International Static Analysis Symposium (SAS 2005), Lecture Notes in Computer Science 3672, pp.352-367, Springer, September, 2005.    2005  [Refereed]

     View Summary

    The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D'Argenio, and Rezk coined the term "self-composition" to describe this reduction. This paper generalizes the self-compositional approach with a form of information downgrading recently proposed by Li and Zdancewic. We also identify a problem with applying the self-compositional approach in practice, and we present a solution to this problem that makes use of more traditional type-based approaches. The result is a framework that combines the best of both worlds, i.e., better than traditional type-based approaches and better than the self-compositional approach.

    DOI

    Scopus

    175
    Citation
    (Scopus)
  • Witnessing side-effects

    T Terauchi, A Aiken

    In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), ACM SIGPLAN Notices 40 (9), pp.105-115, ACM    2005  [Refereed]

     View Summary

    We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a static checking algorithm that makes use of a network flow property equivalent to the semantic condition.

    DOI

    Scopus

    7
    Citation
    (Scopus)
  • Checking and inferring local non-aliasing

    A Aiken, JS Foster, J Kodumal, T Terauchi

    In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), ACM SIGPLAN Notices 38 (5), pp.129-140, ACM    2003  [Refereed]

     View Summary

    In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.

  • Flow-sensitive type qualifiers

    JS Foster, T Terauchi, A Aiken

    In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), ACM SIGPLAN Notices 37 (5), pp.1-12, ACM    2002  [Refereed]

     View Summary

    We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type, qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively-the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.

  • Exploring MARS: developing indoor and outdoor user interfaces to a mobile augmented reality system

    T Hollerer, S Feiner, T Terauchi, G Rashid, D Hallaway

    Computers & Graphics   23 ( 6 ) 779 - 785  1999  [Refereed]

     View Summary

    We describe an experimental mobile augmented reality system (MARS) testbed that employs different user interfaces to allow outdoor and indoor users to access and manage information that is spatially registered with the real world. Outdoor users can experience spatialized multimedia presentations that are presented on a head-tracked, see-through, head-worn display used in conjunction with a hand-held pen-based computer. Indoor users can get an overview of the outdoor scene and communicate with outdoor users through a desktop user interface or a head- and hand-tracked immersive augmented reality user interface. (C) 1999 Elsevier Science Limited. All rights reserved.

    DOI

    Scopus

    300
    Citation
    (Scopus)

▼display all

Awards

  • Grand Prize, Shigeo Tsujii Security Award

    2022.10   Japan Society of Security Management   Repairing DoS Vulnerability of Real-World Regexes

    Winner: Nariyoshi Chida, Tachio Terauchi

  • Best paper award

    2022.03   JSSST The 24th Programming and Programming Language Workshop (PPL 2022)   代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

    Winner: Fuga Kawamata, Tachio Terauchi

  • WASEDA RESEARCH AWARD High-Impact Publication

    2019.12   Waseda University  

    Winner: Tachio Terauchi

  • Nominee, 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   Compositional Synthesis of Leakage Resilient Programs

    Winner: Arthur Blot, Masaki Yamamoto, Tachio Terauchi

  • Best presentation award

    2008.03   JSSST The 10th Programming and Programming Language Workshop (PPL 2008)  

  • 第4回野口研究奨励賞

    2008   情報処理学会 東北支部  

    Winner: 寺内 多智弘

▼display all

Research Projects

  • Dependent refinement types and predicate constraints for program verification

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    Project Year :

    2022.04
    -
    2027.03
     

  • Understanding malware semantics by AI-supported formal methods

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Challenging Research (Pioneering)

    Project Year :

    2020.07
    -
    2026.03
     

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

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research 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

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research 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

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Challenging Research (Exploratory)

    Project Year :

    2018.06
    -
    2021.03
     

    Tachio Terauchi

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

    JSPS  Core-to-Core Program A. Advanced Research Networks.

    Project Year :

    2015.04
    -
    2020.03
     

    Hajime Ishihara

  • Logical and Formal Methods for Information Security - with Special Focus on Cryptographic Protocol Verification and Quantitative Information Flow Analysis

    JSPS  Bilateral Programs (AYAME Program)

    Project Year :

    2016.04
    -
    2019.03
     

    Mitsuhiro Okada

  • Mathematical Structure of Software Verification Based on Practically Efficient Behavior.

    JSPS  Bilateral Programs.

    Project Year :

    2015.04
    -
    2017.12
     

    Shoji Yuen

  • Large scale verification of higher-order programs

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)

    Project Year :

    2014.04
    -
    2017.03
     

    Tachio Terauchi

     View Summary

    The goal of the research is to advance the state of the art on automatic verification techniques of higher-order functional programs. We have especially focused on the techniques based on software model checking via dependent type inference, that has gained popularity in the recent years.
    <BR>
    The main contributions of the research are as follows: 1.) New, improved abstraction refinement methods (abstraction refinement is a technique used in software model checking), 2.) New automatic methods for verification of temporal properties (such as termination and liveness) of higher-order functional programs.

  • Verification of real-time reactive systems in high-level programming languages

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    Project Year :

    2013.04
    -
    2017.03
     

    Yuen Shoji, Tachio Terauchi

     View Summary

    This study presents a safety verification of real-time programs described by a high level programming language with syntax such as recursive calls and interrupt handlings. We proposed a new behavioral model called 'Nested Timed Automata', NeTA for short. The state reachability of NeTA is shown to be decidable. This shows the safety verification is possible. NeTA is a pushdown system whose stack alphabets are timed automata. We also introduced the clock freezing for clocks of timed automata while it is on the stack. It is shown that the reachability is kept decidable under a certain condition. We investigated an efficient Zone-constrcution method to improve the efficiency.

  • Temporal Property Verification of Higher-Order Programs

    JSPS  Postdoctoral Fellowship for Research in Japan.

    Project Year :

    2013
     
     
     

    Tachio Terauchi, Eric Koskinen

  • Verification of Quantitative Information Flow

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B)

    Project Year :

    2011
    -
    2013
     

    Tachio Terauchi

     View Summary

    We solved open problems concerning the complexity of various quantitative information flow verification problems. We considered quantitative information flow definitions based on various information theoretic notions such as belief and min entropy channel capacity, and studied the problems both from the computational complexity theoretic aspect and the program verification property classification aspect formalized by the notion of "hyperproperties." We also proposed algorithms for precisely inferring and verifying the quantitative information flow bounds that utilize software model checking and counting algorithms. We also proposed new approaches to software model checking.

  • Advancement and Application of Type Theory for Improving Software Safety

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

    Project Year :

    2008
    -
    2010
     

    Naoki Kobayashi, Atsushi Igarashi, Eijiro Sumii, Kazutaka Matsuda, Tachio Terauchi

     View Summary

    This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.

  • Verification of Multi-thread Programs via Linear Programming

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B)

    Project Year :

    2008
    -
    2010
     

    Tachio Terauchi

     View Summary

    We propose a software verification framework based on the formalism of fractional capabilities thatstatically (i.e., at compile time) and automatically checksthatcertain bad things (e.g., data races) never happenin concurrent programs. The key to the success is the reduction of fractional capability calculito the problem of linear programming.

▼display all

Presentations

  • Repairing DoS Vulnerability of Real-World Regexes

    Nariyoshi Chida, Tachio Terauchi

    JSSST The 24th Programming and Programming Language Workshop (PPL 2022) 

    Presentation date: 2022.03

  • 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト

    川俣 楓河, 寺内 多智弘

    JSSST The 24th Programming and Programming Language Workshop (PPL 2022) 

    Presentation date: 2022.03

  • 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

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

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

    JSSST The 21st Programming and Programming Language Workshop (PPL 2019) 

    Presentation date: 2019.03

  • A Fixpoint Logic and Dependent Effects for Temporal Property Verification

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

    JSSST The 21st Programming and Programming Language Workshop (PPL 2019) 

    Presentation date: 2019.03

  • On Cut-elimination in Cyclic Proof Systems

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

    The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018) 

    Presentation date: 2018.12

  • Information Flow Security and its Applications to Side Channel Attack Resilience

    Tachio Terauchi  [Invited]

    The 4th Franco-Japanese Workshop on Cybersecurity 

    Presentation date: 2018.05

  • Dependent Temporal Effects and Fixpoint Logic for Verification (Poster Presentation)

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

    JSSST The 20th Programming and Programming Language Workshop (PPL 2018) 

    Presentation date: 2018.03

  • Compositional Synthesis of Leakage Resilient Programs.

    Tachio Terauchi

    NII Shonan Meeting Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security 

    Presentation date: 2018.01

  • On Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [Invited]

    The 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016) 

    Presentation date: 2016.04

  • On Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [Invited]

    NII Shonan Meeting Seminar 078: Higher-Order Model Checking 

    Presentation date: 2016.03

  • Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [Invited]

    Dagstuhl Seminar 16131: Language Based Verification Tools for Functional Programs 

    Presentation date: 2016.03

  • Verification of Object-Oriented Programs via Refinement Types (Poster presentation)

    Nam Mai, Tachio Terauchi

    The 13th Asian Symposium on Programming Languages and Systems (APLAS 2015) 

    Presentation date: 2015.11

  • Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [Invited]

    NII Shonan Meeting Seminar 063: Semantics and Verification of Object-Oriented Languages 

    Presentation date: 2015.09

  • Information Flow Analysis and Applications to Computer Security

    Tachio Terauchi  [Invited]

    NII Shonan Meeting Seminar 065: Low-level Code Analysis and Applications to Computer Security 

    Presentation date: 2015.03

  • 効率の良いLeakage Resilientプログラムの自動生成に向けて (ポスター発表)

    山本真輝, 寺内多智弘

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

    Presentation date: 2015.03

  • プログラム検証とインバリアント生成

    寺内 多智弘  [Invited]

    ソフトウェア科学会第31回全国大会 

    Presentation date: 2014.09

  • On Complexity of Verifying Quantitative Information Flow

    Tachio Terauchi  [Invited]

    Dagstuhl Seminar 12481: Quantitative Security Analysis 

    Presentation date: 2012.11

  • Automated Verification of Higher-Order Functional Programs

    Tachio Terauchi  [Invited]

    The 11th International Symposium on Functional and Logic Programming (FLOPS 2012) 

    Presentation date: 2012.05

  • Relatively Complete Refinement Types from Counterexamples

    Tachio Terauchi  [Invited]

    NII Shonan Meeting Seminar 005: Automated Techniques for Higher-Order Program Verification 

    Presentation date: 2011.09

  • Polymorphic Fractional Capabilities

    Hirotoshi Yasuoka, Tachio Terauchi

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

    Presentation date: 2010.03

  • 量的情報流の検証の困難性と可能性について. (ポスター発表)

    安岡宏俊, 寺内 多智弘

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

    Presentation date: 2010.03

  • Dependent Types from Counterexamples (ポスター発表)

    寺内 多智弘

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

    Presentation date: 2010.03

  • Checking Race Freedom via Linear Programming.

    寺内 多智弘

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

    Presentation date: 2008.03

  • Classification of Cancer Tissue Types by Support Vector Machines using Micro Array Gene Expression Data (Poster presentation)

    Jinsong Cai, Aynur Dayanik, Hong Yu, Naveed Hasan, Tachio Terauchi, William N. Grundy

    The 8th International Conference on Intelligent Systems for Molecular Biology (ISMB 2000) 

    Presentation date: 2000.08

▼display all

 

Syllabus

▼display all

 

Committee Memberships

  • 2020.04
    -
    Now

    JSSST Special Interest Group on Programming and Programming Languages  Steering Committee

  • 2022
    -
    2023

    The 36th IEEE Computer Security Foundations Symposium (CSF 2023)  Program Committee

  • 2022
    -
    2023

    The 32nd European Symposium on Programming (ESOP 2023)  Program Committee

  • 2018.04
    -
    2022.03

    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

  • 2021
    -
    2022

    The 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)  Program Committee

  • 2021
    -
    2022

    The 49th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2022)  Program Committee

  • 2020
    -
    2021

    The International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2021)  Program Committee

  • 2020
    -
    2021

    The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021)  Program Committee

  • 2020
    -
    2021

    The 19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021)  Program Committee

  • 2020
    -
    2021

    The 33rd International Conference on Computer-Aided Verification (CAV 2021)  Program Committee

  • 2020
    -
    2021

    The 34th IEEE Computer Security Foundations Symposium (CSF 2021)  Program Committee

  • 2015.04
    -
    2020.03

    文部科学省 科学技術政策研究所 科学技術動向研究センター  専門調査員

  • 2019
    -
    2020

    The 15th International Symposium on Functional and Logic Programming (FLOPS 2020)  Program Committee

  • 2019
    -
    2020

    JSSST The 22nd Programming and Programming Language Workshop (PPL 2020)  Program Committee

  • 2019
    -
    2020

    The 12th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2020)  Program Committee

  • 2019
    -
    2020

    The 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020)  Program Committee

  • 2018
    -
    2019

    The International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2019)  Program Committee

  • 2018
    -
    2019

    The 26th International Symposium on Static Analysis (SAS 2019)  Program Committee

  • 2018
    -
    2019

    The 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)  Program Committee

  • 2018
    -
    2019

    The 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019)  Program Committee

  • 2018
    -
    2019

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

  • 2014.04
    -
    2018.03

    IPSJ Special Interest Group on Programming  Steering Committee

  • 2017
    -
    2018

    The 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018)  Program Committee

  • 2017
    -
    2018

    The 16th Asian Symposium on Programming Languages and Systems (APLAS 2018)  Program Committee

  • 2017
    -
    2018

    The 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018)  Program Committee

  • 2017
    -
    2018

    The 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)  Program Committee

  • 2016
    -
    2017

    The 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017)  External Review Committee

  • 2016
    -
    2017

    The 26th European Symposium on Programming (ESOP 2017)  Program Committee

  • 2016
    -
    2017

    The 4th International Conference on Tools and Methods of Program Analysis (TMPA 2017)  Program Committee

  • 2016
    -
    2017

    The 11th International Workshop on Reachability Problems (RP 2017)  Program Committee

  • 2016
    -
    2017

    The 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)  Program Committee

  • 2016
    -
    2017

    The 15th Asian Symposium on Programming Languages and Systems (APLAS 2017)  Program Committee

  • 2016
    -
    2017

    NII Shonan Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security  Co-Organizer

  • 2015
    -
    2016

    The 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)  Program Committee

  • 2015
    -
    2016

    The 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) (Track B)  Program Committee

  • 2015
    -
    2016

    The 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016)  External Review Committee

  • 2015
    -
    2016

    The 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)  Program Committee

  • 2015
    -
    2016

    The 14th Asian Symposium on Programming Languages and Systems (APLAS 2016)  Program Committee

  • 2014
    -
    2015

    The 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015)  Program Committee

  • 2014
    -
    2015

    ACM SIGPLAN 10th Workshop on Programming Languages and Analysis for Security (PLAS 2015)  Program Committee

  • 2014
    -
    2015

    Workshop on Higher-Order Program Analysis (HOPA 2015)  Program Committee

  • 2014
    -
    2015

    NII Shonan Seminar 069: Logic and Verification Methods in Security and Privacy  Co-Organizer

  • 2013
    -
    2014

    The 9th Special Section on Formal Approach, IEICE Transactions on Information and Systems  Editor

  • 2013
    -
    2014

    The 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014)  Program Committee

  • 2013
    -
    2014

    The 12th International Symposium on Functional and Logic Programming (FLOPS 2014)  Program Committee

  • 2013
    -
    2014

    Workshop on Higher-Order Program Analysis (HOPA 2014)  Program Committee

  • 2013
    -
    2014

    Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography (FCS-FCC'14)  Program Committee

  • 2012
    -
    2013

    The 8th Special Section on Formal Approach, IEICE Transactions on Information and Systems  Editor

  • 2012
    -
    2013

    The 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)  External Review Committee

  • 2012
    -
    2013

    The 22nd EACSL Annual Conference on Computer Science Logic (CSL 2013)  Program Committee

  • 2011
    -
    2012

    The 7th Special Section on Formal Approach, IEICE Transactions on Information and Systems  Editor

  • 2011
    -
    2012

    The 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)  Program Committee

  • 2011
    -
    2012

    The 10th Asian Symposium on Programming Languages and Systems (APLAS 2012)  Program Committee

  • 2010
    -
    2011

    The 6th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2011)  Program Committee

  • 2010
    -
    2011

    The 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011)  Program Committee

  • 2010
    -
    2011

    The 10th International Conference on Typed Lambda Calculi and Applications (TLCA 2011)  Program Committee

  • 2010
    -
    2011

    The 5th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2011)  Program Committee

  • 2010
    -
    2011

    The 20th European Symposium on Programming (ESOP 2011)  Program Committee

  • 2010
    -
    2011

    The 10th International Conference on Typed Lambda Calculi and Applications (TLCA 2011)  Program Committee

  • 2009
    -
    2010

    ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI 2010)  External Review Committee

  • 2009
    -
    2010

    JSSST The 12th Programming and Programming Language Workshop (PPL 2010)  Program Co-Chair

  • 2009
     
     

    JSSST The 11th Programming and Programming Language Workshop (PPL 2020)  Program Committee

  • 2008
    -
    2009

    ACM SIGPLAN 4th Workshop on Programming Languages and Analysis for Security (PLAS 2009)  Program Committee

  • 2008
    -
    2009

    The 24th Annual ACM Symposium on Applied Computing (ACM SAC 2009) (Programming Languages Track)  Program Committee

  • 2007
    -
    2008

    The 15th International Static Analysis Symposium (SAS 2008)  Program Committee

▼display all