2022/01/21 更新

写真a

テラウチ タチオ
寺内 多智弘
所属
理工学術院 基幹理工学部
職名
教授
プロフィール
プログラミング言語分野の研究を行っています。特に、プログラムの正しさを正式かつ(できるだけ)自動的に検証する「プログラム検証」や正しいプログラムを自動生成する「プログラム合成」の研究に興味があります。また、型システムや定理証明など基礎理論・基礎アルゴリズムに関する研究も行っています。

学内研究所等

  • 2020年
    -
    2022年

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

学歴

  • 2000年09月
    -
    2006年08月

    カリフォルニア大学バークレー校   電子工学・コンピュータサイエンス学科   コンピュータサイエンス専攻  

  • 1996年09月
    -
    2000年05月

    コロンビア大学   工学・応用科学科   コンピュータサイエンス専攻  

学位

  • カリフォルニア大学バークレー校   博士

  • カリフォルニア大学バークレー校   修士

  • コロンビア大学   学士

経歴

  • 2017年09月
    -
    継続中

    早稲田大学   理工学術院 基幹理工学部 情報理工学科   教授

  • 2014年04月
    -
    2017年09月

    北陸先端科学技術大学院大学   情報科学研究科   教授

  • 2011年04月
    -
    2014年03月

    名古屋大学   大学院情報科学研究科   准教授

  • 2007年01月
    -
    2011年03月

    東北大学   大学院情報科学研究科   助教

所属学協会

  •  
     
     

    ACM

  •  
     
     

    情報処理学会

  •  
     
     

    ソフトウェア科学会

 

研究分野

  • 情報学基礎論

  • ソフトウェア

研究キーワード

  • プログラミング言語

  • プログラム検証

  • プログラム合成

  • 型システム

  • 自動定理証明

  • セキュリティ

▼全件表示

論文

  • 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年  [査読有り]

    DOI

  • Bucketing and Information Flow Analysis for Provable Timing Attack Mitigation

    Tachio Terauchi, Timos Antonopoulos

    Journal of Computer Security   28 ( 6 ) 607 - 634  2020年  [査読有り]  [国際誌]  [国際共著]

    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年  [査読有り]  [招待有り]  [国内誌]

     概要を見る

    <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年  [査読有り]  [国際誌]

    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年  [査読有り]  [国際誌]

    DOI

  • 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年  [査読有り]  [国際誌]

    DOI

  • 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年  [査読有り]  [国際誌]

    DOI

  • 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年  [査読有り]  [国際誌]

     概要を見る

    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

  • 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年  [査読有り]  [国際誌]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • Quantitative information flow as safety and liveness hyperproperties

    Hirotoshi Yasuoka, Tachio Terauchi

    Theoretical Computer Science   538   167 - 182  2014年  [査読有り]

     概要を見る

    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

  • 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月  [査読有り]

     概要を見る

    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

  • 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて

    岩塚 卓弥, 寺内 多智弘, 結縁 祥治

    情報処理学会論文誌プログラミング(PRO)   6 ( 3 ) 20 - 32  2013年  [査読有り]

    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年  [査読有り]

     概要を見る

    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

  • On bounding problems of quantitative information flow

    Hirotoshi Yasuoka, Tachio Terauchi

    Journal of Computer Security   19 ( 6 ) 1029 - 1082  2011年  [査読有り]  [招待有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • Witnessing side effects

    Tachio Terauchi, Alex Aiken

    ACM Transactions on Programming Languages and Systems (TOPLAS)   30 ( 3 ) 15:1-15:42  2008年05月  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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

  • 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年  [査読有り]

     概要を見る

    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年  [査読有り]

     概要を見る

    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年  [査読有り]

     概要を見る

    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

▼全件表示

受賞

  • 早稲田大学リサーチアワード 国際研究発信力

    2019年12月   早稲田大学  

    受賞者: 寺内 多智弘

  • 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  

    受賞者: Arthur Blot, Masaki Yamamoto, Tachio Terauchi

  • 発表賞(一般)

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

    受賞者: 寺内 多智弘

  • 第4回野口研究奨励賞

    2008年   情報処理学会 東北支部  

    受賞者: 寺内 多智弘

共同研究・競争的資金等の研究課題

  • 数理論理手法と人工知能手法の融合に基づくマルウェアの自動意味理解

    日本学術振興会  科学研究費助成事業 挑戦的研究(開拓)

    研究期間:

    2020年07月
    -
    2026年03月
     

    小川 瑞史, NGUYEN MinhLe, 寺内 多智弘, 関 浩之

  • 時相的・関係的仕様からの高レベルプログラム合成

    日本学術振興会  科学研究費助成事業 基盤研究(B)

    研究期間:

    2020年04月
    -
    2025年03月
     

    海野 広志, 南出 靖彦, 寺内 多智弘

  • 高階・再帰的データ構造への破壊的代入を含む高レベル言語プログラムの高精度な検証

    日本学術振興会  科学研究費助成事業 基盤研究(B)

    研究期間:

    2017年04月
    -
    2022年03月
     

    寺内 多智弘, 海野 広志

     概要を見る

    依存型・依存エフェクトシステムと一階述語不動点論理(first-order fixpoint logic)による高階プログラムの時相論理仕様検証に関する研究を行った。研究の成果をまとめた論文は理論計算機科学分野におけるトップ国際会議LICS 2018に採録された。また、関連して、一階述語不動点論理式の真偽性を解く自動定理証明アルゴリズムの研究および一階述語不動点論理による双模倣性の検証などのについても研究を推進し、The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)およびThird Workshop on Mathematical Logic and its Applications (MLA 2019)にてこの研究に関する講演を行った。
    <BR>
    また、循環証明(cyclic proof)と分離論理(separation logic)に関する研究も行った。具体的には、循環証明による分離論理の定理証明は、再帰データ構造を含む場合カット除去不可能であることを示した。この研究に関してThe 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)、日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)およびMLA2019にて講演を行った。
    <BR>
    加えて、サイドチャネル攻撃に対する耐タンパ性の検証など情報セキュリティに関するプログラム検証の研究を行った。

  • サイドチャネル攻撃耐タンパ性のためのプログラム検証・プログラム合成技術

    日本学術振興会  科学研究費助成事業 挑戦的研究(萌芽)

    研究期間:

    2018年06月
    -
    2021年03月
     

    寺内 多智弘

     概要を見る

    代表的なサイドチャネル攻撃の一つであるタイミング攻撃に関する研究を行った。具体的には、bucketingというプログラム変換によるタイミング攻撃に対する防衛手法について研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。これら、必要条件・十分条件は解析対象システムの正規チャネルとサイドチャネルの安全性を分離して議論することを可能とする枠組みであり、また、過去の観測に依存した動作を行える強力なadaptiveな攻撃者を考慮している。この研究の成果をまとめた論文はセキュリティに関する国際会議The 8th International Conference on Principles of Security and Trust (POST 2019)に採録された。
    <BR>
    加えて、一階述語不動点論理による時相仕様検証や循環証明による分離論理のための定理証明など、関連するより一般的なプログラム検証および定理証明についての研究も行った。

  • 数理論理学とその応用の国際研究拠点形成

    日本学術振興会  研究拠点形成事業 先端拠点形成型

    研究期間:

    2015年04月
    -
    2020年03月
     

    石原 哉

  • 論理的ー形式的手法による情報セキュリティ研究ー暗号プロトコル検証と量的情報流解析

    日本学術振興会  二国間交流事業 共同研究 (AYAMEプログラム)

    研究期間:

    2016年04月
    -
    2019年03月
     

    岡田 光弘

  • 実用効率の振舞いに基づくソフトウェア検証の数理的構造

    日本学術振興会  二国間交流事業 共同研究

    研究期間:

    2015年04月
    -
    2017年12月
     

    結縁 祥治

  • 高階プログラミング言語で記述された大規模ソフトウェアの検証

    日本学術振興会  科学研究費助成事業 基盤研究(C)

    研究期間:

    2014年04月
    -
    2017年03月
     

    寺内 多智弘

     概要を見る

    本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。
    <BR>
    主な研究成果は以下である:1.)よりよい抽象詳細化(ソフトウェアモデル検査に用いられる技術)の手法、2.)高階関数型プログラムのための停止性・活性仕様など時相論理仕様の自動検証手法。

  • 高レベル言語で記述されたリアクティブシステムに対する実時間性質の検証

    日本学術振興会  科学研究費助成事業 基盤研究(B)

    研究期間:

    2013年04月
    -
    2017年03月
     

    結縁 祥治, 寺内 多智弘

     概要を見る

    本研究では、再帰呼び出しや割り込みなどの手続き呼び出しを持つ高レベル言語で記述された実時間プログラムの振舞いをモデル化するNested Timed Automaton(以下NeTA)を提案し、到達可能性が決定可能であることを示し、安全性検証が可能であることを示した。NeTAは、時間オートマトンをスタックアルファベットに持つプッシュダウンシステムである。さらに、時間オートマトンがスタック上にあるときにクロックを凍結する機構を導入しても、一定の条件のもとで到達可能性が保存することを示した。さらに、効率的なゾーン構成による検証手法について検討した。

  • 高階プログラムのための時相論理仕様検証

    日本学術振興会  外国人特別研究員(欧米短期)事業

    研究期間:

    2013年
     
     
     

    寺内 多智弘

  • 量的情報流の正確な検証

    日本学術振興会  科学研究費助成事業 若手研究(B)

    研究期間:

    2011年
    -
    2013年
     

    寺内 多智弘

     概要を見る

    量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。

  • ソフトウェアの安全性向上のための型理論の深化と応用

    日本学術振興会  科学研究費助成事業 基盤研究(A)

    研究期間:

    2008年
    -
    2010年
     

    小林 直樹, 五十嵐 淳, 住井 英二郎, 松田 一孝, 寺内 多智弘

     概要を見る

    本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.

  • 型理論と線形計画法によるマルチスレッドプログラムの安全性検証

    日本学術振興会  科学研究費助成事業 若手研究(B)

    研究期間:

    2008年
    -
    2010年
     

    寺内 多智弘

     概要を見る

    本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性(例えば、レース状態が起こらないなど)を静的(つまりコンパイル時に)検証する研究である。具体的には「分数権限計算」(FractionalCapability Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。

  • -

▼全件表示

講演・口頭発表等

  • Constraint-based Relational Verification

    Tachio Terauchi  [招待有り]

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

    発表年月: 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)  

    発表年月: 2019年12月

  • A Fixpoint Logic and Dependent Effects for Temporal Property Verification

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 19371: Deduction Beyond Satisfiability  

    発表年月: 2019年09月

  • Solving First-Order Fixpoint Logic for Program Verification

    Tachio Terauchi  [招待有り]

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

    発表年月: 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)  

    発表年月: 2019年03月

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

    Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno

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

    発表年月: 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)  

    発表年月: 2018年12月

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

    Tachio Terauchi  [招待有り]

    The 4th Franco-Japanese Workshop on Cybersecurity  

    発表年月: 2018年05月

  • Dependent Temporal Effects and Fixpoint Logic for Verification (ポスター発表)

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi

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

    発表年月: 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  

    発表年月: 2018年01月

  • On Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [招待有り]

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

    発表年月: 2016年04月

  • On Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

    NII Shonan Meeting Seminar 078: Higher-Order Model Checking  

    発表年月: 2016年03月

  • Temporal Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 16131: Language Based Verification Tools for Functional Programs  

    発表年月: 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)  

    発表年月: 2015年11月

  • Predicate Refinement Heuristics in Program Verification with CEGAR

    Tachio Terauchi  [招待有り]

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

    発表年月: 2015年09月

  • Information Flow Analysis and Applications to Computer Security

    Tachio Terauchi  [招待有り]

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

    発表年月: 2015年03月

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

    山本真輝, 寺内多智弘

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

    発表年月: 2015年03月

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

    寺内 多智弘  [招待有り]

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

    発表年月: 2014年09月

  • On Complexity of Verifying Quantitative Information Flow

    Tachio Terauchi  [招待有り]

    Dagstuhl Seminar 12481: Quantitative Security Analysis  

    発表年月: 2012年11月

  • Automated Verification of Higher-Order Functional Programs

    Tachio Terauchi  [招待有り]

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

    発表年月: 2012年05月

  • Relatively Complete Refinement Types from Counterexamples

    Tachio Terauchi  [招待有り]

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

    発表年月: 2011年09月

  • Polymorphic Fractional Capabilities

    Hirotoshi Yasuoka, Tachio Terauchi

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

    発表年月: 2010年03月

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

    安岡宏俊, 寺内 多智弘

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

    発表年月: 2010年03月

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

    寺内 多智弘

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

    発表年月: 2010年03月

  • Checking Race Freedom via Linear Programming.

    寺内 多智弘

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

    発表年月: 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)  

    発表年月: 2000年08月

▼全件表示

 

現在担当している科目

▼全件表示

 

委員歴

  • 2020年04月
    -
    継続中

    ソフトウェア科学会 プログラミング論研究会  運営委員

  • 2018年04月
    -
    継続中

    情報処理学会プログラミング研究会(PRO)  幹事

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

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

  • 2021年
    -
    2022年

    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年

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

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

    情報処理学会プログラミング研究会(PRO)  運営委員

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

    電子情報通信学会 論文誌 第9回フォーマルアプローチ特集  編集委員

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

    電子情報通信学会 論文誌 第8回フォーマルアプローチ特集  編集委員

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

    電子情報通信学会 論文誌 第7回フォーマルアプローチ特集  編集委員

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

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

  • 2009年
     
     

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

  • 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

▼全件表示