If you made any changes in Pure these will be visible here soon.

Research Output 1999 2019

  • 1006 Citations
  • 12 h-Index
  • 25 Conference contribution
  • 12 Article
2019

A Formal Analysis of Timing Channel Security via Bucketing

Terauchi, T. & Antonopoulos, T., 2019 Jan 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. (eds.). Springer-Verlag, p. 29-50 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11426 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
Formal Analysis
Adaptive systems
Timing
Attack
Time Constant

Games for security under adaptive adversaries

Antonopoulos, T. & Terauchi, T., 2019 Jun, 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; vol. 2019-June).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Adaptive systems
2018
3 Citations (Scopus)

A fixpoint logic and dependent effects for temporal property verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Fixpoint
Automation
Logic
Dependent
Reasoning
2017
3 Citations (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, Vol. 10204 LNCS. p. 277-297 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10204 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Leakage
Synthesis
Threshold Model
Resilience
Compositionality
29 Citations (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 Jun 14, PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, Vol. Part F128414. p. 362-375 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Temporal verification of higher-order functional programs

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Acoustic waves
4 Citations (Scopus)

Temporal verification of higher-order functional programs

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

Research output: Contribution to journalArticle

Acoustic waves
2015
1 Citation (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, Vol. 9291. p. 128-144 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9291).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Program Verification
Refinement
Heuristics
Predicate
Counterexample
4 Citations (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, Vol. 9035. p. 149-163 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9035).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Horn clause
Recursion
Sampling
Constraint Solving
Refinement
1 Citation (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, Vol. 9032. p. 610-633 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9032).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Stratification
Predicate
Refinement
Counterexample
Surface mount technology
2014
17 Citations (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, Vol. 8410 LNCS. p. 392-411 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8410 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Termination
Higher Order
Ranking Function
Reachability Analysis
Soundness
8 Citations (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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Temporal Reasoning
Temporal logic
Specifications
Safety
Trace
11 Citations (Scopus)

Quantitative information flow as safety and liveness hyperproperties

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

Research output: Contribution to journalArticle

Liveness
Information Flow
Safety
Hardness
Reachability
2013
9 Citations (Scopus)

Automating relatively complete verification of higher-order functional programs

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

Research output: Contribution to journalArticle

15 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2012
3 Citations (Scopus)

Quantitative information flow as safety and liveness hyperproperties

Yasuoka, H. & Terauchi, T., 2012 Jul 3, In : Electronic Proceedings in Theoretical Computer Science, EPTCS. 85, p. 77-91 15 p.

Research output: Contribution to journalArticle

Hardness
Chemical analysis
2011
11 Citations (Scopus)

On bounding problems of quantitative information flow

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

Research output: Contribution to journalArticle

Entropy
Hardness
Channel capacity
Chemical analysis
2010
8 Citations (Scopus)

Dependent types from counterexamples

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

Research output: Contribution to journalArticle

Recursive functions
Model checking
29 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Recursive functions
Model checking
11 Citations (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. Vol. 6345 LNCS. p. 357-372 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6345 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Information Flow
Entropy
Noninterference
Shannon Entropy
Hardness
38 Citations (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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Entropy
Hardness
Channel capacity
Chemical analysis
2009
4 Citations (Scopus)

Polymorphic fractional capabilities

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Fractional
Static analysis
Polymorphism
Linear programming
Calculus
2008
21 Citations (Scopus)

A capability calculus for concurrency and determinism

Terauchi, T. & Aiken, A., 2008 Aug 1, In : ACM Transactions on Programming Languages and Systems. 30, 5, 27.

Research output: Contribution to journalArticle

Polynomials
Communication
24 Citations (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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Polynomials
23 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Linear programming
Static analysis
Joining
Synchronization
2 Citations (Scopus)

Checking race freedom via linear programming

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

Research output: Contribution to journalArticle

Linear programming
Static analysis
Joining
Synchronization
1 Citation (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. Vol. 4960 LNCS. p. 284-298 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4960 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Static analysis
Linear programming
Buffer
Casting
Polynomials
3 Citations (Scopus)

Witnessing side effects

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

Research output: Contribution to journalArticle

Semantics
2006
9 Citations (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, Vol. 4137 LNCS. p. 218-232 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4137 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Determinism
Confluence
Communication Channels
Concurrency
Concurrent
3 Citations (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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Context free languages
Turing machines
Recursion
Undecidability
Intersection
2005
135 Citations (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). Vol. 3672 LNCS. p. 352-367 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 3672 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Information Flow
Safety
Chemical analysis
Program Transformation
Termination
7 Citations (Scopus)

Witnessing side-effects

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

Research output: Contribution to journalArticle

Semantics
4 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
2003
9 Citations (Scopus)

Checking and inferring local non-aliasing

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

Research output: Contribution to journalArticle

Experiments
Linux
45 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Experiments
Linux
2002
240 Citations (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.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Linux
1999
265 Citations (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, In : Computers and Graphics (Pergamon). 23, 6, p. 779-785 7 p.

Research output: Contribution to journalArticle

Augmented reality
User interfaces
Testbeds
Display devices