TOP > 研究活動 > 研究者総覧「情報知」 > 情報システム学専攻 > ソフトウェア論講座 > 寺内　多智弘

研究者総覧「情報知」

情報システム学専攻

氏　名
寺内　多智弘（てらうち　たちお）
講座等
ソフトウェア論講座
職　名
准教授
学　位
Ph.D.
研究分野
プログラミング言語

研究内容

プログラム解析とプログラム検証
[背景]
現在、コンピュータ及び様々な電子機器を動かしているのは「プログラム」です。携帯のアプリもカーナビも飛行機の制御システムもMacOS・Windowsなどのオペレーティングシステムも、全てプログラムで動いています。プログラムは人間の書くものであるため、プログラミングの間違いにより、コンピュータの誤作動・不具合に至ることがあります。

例えば、C言語のプログラムで、外部から入力として渡された値の範囲をチェックせず配列のインデックスとして使用すると、配列外のメモリのアクセスが起こり重大なシステムのエラーに繋がることがあります。プログラム解析・プログラム検証とは、こうしたプログラムの不具合(つまりバグ)の検出および防止を、プログラミング言語理論の技術を応用して行うというものです。プログラム解析・プログラム検証は、元々は、コンパイラ最適化のために提案されたものですが、近年では、こうした不具合検出・防止の用途に用いる研究が盛んに行われています。具体的には、モデル検査・抽象解釈・定理証明・型システムなど、複数の視点からの研究が進められています。

[研究内容]
私のウェブページをご参考に下さい。
http://www.sqlab.i.is.nagoya-u.ac.jp/~terauchi/index-j.html

 

経歴

  • 2000年 コロンビア大学 卒業
  • 2004年 カリフォルニア大学バークレー校 修士号取得
  • 2006年 カリフォルニア大学バークレー校 博士号取得
  • 2007年 東北大学大学院 情報科学研究科 助教
  • 2011年 名古屋大学大学院 情報科学研究科 准教授

所属学会

主要論文・著書

  1. Hirotoshi Yasuoka and Tachio Terauchi. On Bounding Problems of Quantitative Information Flow. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science 6345, Springer, 2010. pp.357-372.
  2. Hirotoshi Yasuoka and Tachio Terauchi. Quantitative Information Flow - Verification Hardness and Possibilities. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society, 2010. pp.15-27.
  3. Tachio Terauchi. Dependent Types from Counterexamples. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), ACM, 2010. pp.119-130.
  4. Hirotoshi Yasuoka and Tachio Terauchi. Polymorphic Fractional Capabilities. In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science 5673, Springer, 2009. pp.36-51.
  5. Tachio Terauchi. A Type System for Observational Determinism. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), IEEE Computer Society, 2008. pp.287-300.
  6. Tachio Terauchi. Checking Race Freedom via Linear Programming. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), ACM, 2008. pp.1-10.
  7. Tachio Terauchi and Adam Megacz. Inferring Channel Buffer Bounds via Linear Programming. In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science 4960, Springer, 2008. pp.284-298.
  8. Tachio Terauchi and Alex Aiken. A Capability Calculus for Concurrency and Determinism. In Proceedings of the 17th International Conference on Concurrency Theory (CONCUR 2006), Lecture Notes in Computer Science 4137, Springer, 2006. pp.218-232.
  9. Tachio Terauchi and Alex Aiken. On Typability for Rank-2 Intersection Types with Polymorphic Recursion. In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006), IEEE Computer Society, 2006. pp.111-122.
  10. Tachio Terauchi and Alex Aiken. Witnessing Side-Effects. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), ACM, 2005. pp.105-115.
  11. Tachio Terauchi and Alex Aiken. Secure Information Flow as a Safety Problem. In Proceedings of the 12th International Static Analysis Symposium (SAS 2005), Lecture Notes in Computer Science 3672, Springer, 2005. pp.352-367.
  12. Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi. Checking and Inferring Local Non-Aliasing. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), ACM, 2003. pp.129-140.
  13. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-Sensitive Type Qualifiers. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), ACM, 2002. pp.1-12.
  14. Tachio Terauchi and Alex Aiken. A Capability Calculus for Concurrency and Determinism. ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5) : (2008)
  15. Tachio Terauchi and Alex Aiken. Witnessing Side Effects. ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (3) : (2008)
  16. Tobias H\"ollerer, Steven Feiner, Tachio Terauchi, Gus Rashid, and Drexel Hallaway. Exploring MARS: Developing Indoor and Outdoor User Interfaces to a Mobile Augmented Reality System. Computers \& Graphics 23 (6) : 779-785 (1999)
  17. Hirotoshi Yasuoka, Tachio Terauchi: On bounding problems of quantitative information flow. Journal of Computer Security 19(6): 1029-1082 (2011)
  18. Hirotoshi Yasuoka, Tachio Terauchi: Quantitative Information Flow as Safety and Liveness Hyperproperties. In Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science 85, 2012 : 77-91
  19. Tachio Terauchi: Automated Verification of Higher-Order Functional Programs. In Proceedings of the 11th International Symposium on Functional and Logic Programming - 11th International Symposium (FLOPS 2012), Lecture Notes in Computer Science 7294, Springer, 2012
  20. Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi: Automating relatively complete verification of higher-order functional programs. In Proceedings of the 40th ACM Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), ACM, 2013 : 75-86

BACK

このページのトップへ