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

研究成果 1999 2019

  • 1004 引用
  • 12 h指数
  • 25 Conference contribution
  • 12 Article
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

Games for security under adaptive adversaries

Antonopoulos, T. & Terauchi, T., 2019 6, Proceedings - 2019 IEEE 32nd Computer Security Foundations Symposium, CSF 2019. IEEE Computer Society, p. 216-229 14 p. 8823693. (Proceedings - IEEE Computer Security Foundations Symposium; 巻数 2019-June).

研究成果: Conference contribution

Game theory
Security systems
Adaptive systems
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
3 引用 (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
29 引用 (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
4 引用 (Scopus)

Temporal verification of higher-order functional programs

Murase, A., Terauchi, T., Kobayashi, N., Sato, R. & Unno, H., 2016 4 8, : : ACM SIGPLAN Notices. 51, 1, p. 57-68 12 p.

研究成果: Article

Acoustic waves
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
11 引用 (Scopus)

Quantitative information flow as safety and liveness hyperproperties

Yasuoka, H. & Terauchi, T., 2014, : : Theoretical Computer Science. 538, C, p. 167-182 16 p.

研究成果: Article

Liveness
Information Flow
Safety
Hardness
Reachability
2013
9 引用 (Scopus)

Automating relatively complete verification of higher-order functional programs

Unno, H., Terauchi, T. & Kobayashi, N., 2013 1, : : ACM SIGPLAN Notices. 48, 1, p. 75-86 12 p.

研究成果: Article

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

2012
3 引用 (Scopus)
Hardness
Chemical analysis
2011
11 引用 (Scopus)

On bounding problems of quantitative information flow

Yasuoka, H. & Terauchi, T., 2011, : : Journal of Computer Security. 19, 6, p. 1029-1082 54 p.

研究成果: Article

Entropy
Hardness
Channel capacity
Chemical analysis
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
8 引用 (Scopus)

Dependent types from counterexamples

Terauchi, T., 2010 1, : : ACM SIGPLAN Notices. 45, 1, p. 119-130 12 p.

研究成果: Article

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
38 引用 (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
21 引用 (Scopus)
Polynomials
Communication
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
2 引用 (Scopus)

Checking race freedom via linear programming

Terauchi, T., 2008 6, : : ACM SIGPLAN Notices. 43, 6, p. 1-10 10 p.

研究成果: Article

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
3 引用 (Scopus)

Witnessing side effects

Terauchi, T. & Aiken, A., 2008 5 1, : : ACM Transactions on Programming Languages and Systems. 30, 3, 15.

研究成果: Article

Semantics
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
134 引用 (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
7 引用 (Scopus)

Witnessing side-effects

Terauchi, T. & Aiken, A., 2005, : : ACM SIGPLAN Notices. 40, 9, p. 105-115 11 p.

研究成果: Article

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
9 引用 (Scopus)

Checking and inferring local non-aliasing

Aiken, A., Foster, J. S., Kodumal, J. & Terauchi, T., 2003 5, : : ACM SIGPLAN Notices. 38, 5, p. 129-140 12 p.

研究成果: Article

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
1999
265 引用 (Scopus)

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

Höllerer, T., Feiner, S., Terauchi, T., Rashid, G. & Hallaway, D., 1999, : : Computers and Graphics (Pergamon). 23, 6, p. 779-785 7 p.

研究成果: Article

Augmented reality
User interfaces
Testbeds
Display devices