• 991 引用
  • 12 h指数
19992019
Pureに変更を加えた場合、すぐここに表示されます。

研究成果 1999 2019

  • 991 引用
  • 12 h指数
  • 24 Conference contribution
  • 12 Article
フィルター
Conference contribution
2019

A Formal Analysis of Timing Channel Security via Bucketing

Terauchi, T. & Antonopoulos, T., 2019 1 1, Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Nielson, F. & Sands, D. (版). Springer-Verlag, p. 29-50 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 11426 LNCS).

研究成果: Conference contribution

公開
Formal Analysis
Adaptive systems
Timing
Attack
Time Constant
2018
3 引用 (Scopus)

A fixpoint logic and dependent effects for temporal property verification

Nanjo, Y., Unno, H., Koskinen, E. & Terauchi, T., 2018 7 9, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Institute of Electrical and Electronics Engineers Inc., 巻 Part F138033. p. 759-768 10 p.

研究成果: Conference contribution

Fixpoint
Automation
Logic
Dependent
Reasoning
2017
2 引用 (Scopus)

Compositional synthesis of leakage resilient programs

Blot, A., Yamamoto, M. & Terauchi, T., 2017, Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Springer Verlag, 巻 10204 LNCS. p. 277-297 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 10204 LNCS).

研究成果: Conference contribution

Leakage
Synthesis
Threshold Model
Resilience
Compositionality
25 引用 (Scopus)

Decomposition instead of self-composition for proving the absence of timing channels

Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T. & Wei, S., 2017 6 14, PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, 巻 Part F128414. p. 362-375 14 p.

研究成果: Conference contribution

Decomposition
Chemical analysis
Acoustic waves
Specifications
Side channel attack
2016
6 引用 (Scopus)

Temporal verification of higher-order functional programs

Murase, A., Terauchi, T., Kobayashi, N., Sato, R. & Unno, H., 2016 1 11, POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, 巻 20-22-January-2016. p. 57-68 12 p.

研究成果: Conference contribution

Acoustic waves
2015
1 引用 (Scopus)

Explaining the effectiveness of small refinement heuristics in program verification with CEGAR

Terauchi, T., 2015, Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Springer Verlag, 巻 9291. p. 128-144 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 9291).

研究成果: Conference contribution

Program Verification
Refinement
Heuristics
Predicate
Counterexample
4 引用 (Scopus)

Inferring simple solutions to recursion-free horn clauses via sampling

Unno, H. & Terauchi, T., 2015, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Springer Verlag, 巻 9035. p. 149-163 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 9035).

研究成果: Conference contribution

Horn clause
Recursion
Sampling
Constraint Solving
Refinement
1 引用 (Scopus)

Relaxed stratification: A new approach to practical complete predicate refinement

Terauchi, T. & Unno, H., 2015, Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Springer Verlag, 巻 9032. p. 610-633 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 9032).

研究成果: Conference contribution

Stratification
Predicate
Refinement
Counterexample
Surface mount technology
2014
16 引用 (Scopus)

Automatic termination verification for higher-order functional programs

Kuwahara, T., Terauchi, T., Unno, H. & Kobayashi, N., 2014, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, 巻 8410 LNCS. p. 392-411 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 8410 LNCS).

研究成果: Conference contribution

Termination
Higher Order
Ranking Function
Reachability Analysis
Soundness
8 引用 (Scopus)

Local temporal reasoning

Koskinen, E. & Terauchi, T., 2014, Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014. Association for Computing Machinery, 59

研究成果: Conference contribution

Temporal Reasoning
Temporal logic
Specifications
Safety
Trace
2013
15 引用 (Scopus)

Automating relatively complete verification of higher-order functional programs

Unno, H., Terauchi, T. & Kobayashi, N., 2013, POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 75-86 12 p.

研究成果: Conference contribution

2010
29 引用 (Scopus)

Dependent types from counterexamples

Terauchi, T., 2010, POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 119-130 12 p.

研究成果: Conference contribution

Recursive functions
Model checking
11 引用 (Scopus)

On bounding problems of quantitative information flow

Yasuoka, H. & Terauchi, T., 2010, Computer Security, ESORICS 2010 - 15th European Symposium on Research in Computer Security, Proceedings. 巻 6345 LNCS. p. 357-372 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 6345 LNCS).

研究成果: Conference contribution

Information Flow
Entropy
Noninterference
Shannon Entropy
Hardness
36 引用 (Scopus)

Quantitative information flow-verification hardness and possibilities

Hirotoshi, Y. & Terauchi, T., 2010, 23rd IEEE Computer Security Foundations Symposium, CSF 2010. p. 15-27 13 p. 5552655

研究成果: Conference contribution

Entropy
Hardness
Channel capacity
Chemical analysis
2009
4 引用 (Scopus)

Polymorphic fractional capabilities

Yasuoka, H. & Terauchi, T., 2009, Static Analysis - 16th International Symposium, SAS 2009, Proceedings. 巻 5673 LNCS. p. 36-51 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 5673 LNCS).

研究成果: Conference contribution

Fractional
Static analysis
Polymorphism
Linear programming
Calculus
2008
24 引用 (Scopus)

A type system for observational determinism

Terauchi, T., 2008, Proceedings - 21st IEEE Computer Security Foundations Symposium, CSF 2008. p. 287-300 14 p. 4556693

研究成果: Conference contribution

Polynomials
23 引用 (Scopus)

Checking race freedom via linear programming

Terauchi, T., 2008, PLDI'08: Proceedings of the 2008 SIGPLAN Conference on Programming Language Design and Implementation. p. 1-10 10 p.

研究成果: Conference contribution

Linear programming
Static analysis
Joining
Synchronization
1 引用 (Scopus)

Inferring channel buffer bounds via linear programming

Terauchi, T. & Megacz, A., 2008, Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. 巻 4960 LNCS. p. 284-298 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 4960 LNCS).

研究成果: Conference contribution

Static analysis
Linear programming
Buffer
Casting
Polynomials
2006
9 引用 (Scopus)

A capability calculus for concurrency and determinism

Terauchi, T. & Aiken, A., 2006, CONCUR 2006 - Concurrency Theory - 17th International Conference, CONCUR 2006, Proceedings. Springer Verlag, 巻 4137 LNCS. p. 218-232 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 4137 LNCS).

研究成果: Conference contribution

Determinism
Confluence
Communication Channels
Concurrency
Concurrent
3 引用 (Scopus)

On typability for rank-2 intersection types with polymorphic recursion

Terauchi, T. & Aiken, A., 2006, Proceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006. p. 111-120 10 p. 1691222

研究成果: Conference contribution

Context free languages
Turing machines
Recursion
Undecidability
Intersection
2005
132 引用 (Scopus)

Secure information flow as a safety problem

Terauchi, T. & Aiken, A., 2005, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 巻 3672 LNCS. p. 352-367 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 3672 LNCS).

研究成果: Conference contribution

Information Flow
Safety
Chemical analysis
Program Transformation
Termination
4 引用 (Scopus)

Witnessing side-effects

Terauchi, T. & Aiken, A., 2005, ICFP 2005 - Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming. p. 105-115 11 p.

研究成果: Conference contribution

Semantics
2003
45 引用 (Scopus)

Checking and inferring local non-aliasing

Aiken, A., Foster, J. S., Kodumal, J. & Terauchi, T., 2003, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). p. 129-140 12 p.

研究成果: Conference contribution

Experiments
Linux
2002
240 引用 (Scopus)

Flow-sensitive type qualifiers

Foster, J. S., Terauchi, T. & Aiken, A., 2002, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). p. 1-12 12 p.

研究成果: Conference contribution

Linux