Terauchi Tachio 寺内多智弘

… Alternative Names

TERAUCHI Tachio 寺内多智弘

Less

Researcher Number	70447150
Other IDs
Affiliation (Current)	2025: 早稲田大学, 理工学術院, 教授
Affiliation (based on the past Project Information) *help	2017 – 2024: 早稲田大学, 理工学術院, 教授 2016: 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 2014 – 2016: 北陸先端科学技術大学院大学, 情報科学研究科, 教授 2011 – 2013: 名古屋大学, 情報科学研究科, 准教授 2007 – 2010: 東北大学, 大学院・情報科学研究科, 助教
Review Section/Research Field	Principal Investigator Software / Software / Basic Section 60050:Software-related / Medium-sized Section 60:Information science, computer engineering, and related fields Except Principal Investigator Software / Fundamental theory of informatics / Basic Section 60050:Software-related / Medium-sized Section 60:Information science, computer engineering, and related fields / Software
Keywords	Principal Investigator プログラム検証 / 型システム / ソフトウェアモデル検査 / 代数的エフェクト / 自動定理証明 / 不動点論理 / 情報セキュリティ / プログラミング言語 / 型理論 / ソフトウェア検証 … More / 述語制約解消 / 述語制約 / 依存篩型 / プログラム合成 / 耐タンパ性 / サイドチャネル攻撃 / プログラム論理 / 循環証明 / 分離論理 / 停止性検証 / 述語抽象 / 抽象解釈 / 時相論理仕様 / 時相論理 / 抽象詳細化 / 述語論理 / 高階関数 / モデル検査 / プログラム解析 / 量的情報流 / セキュリティ / 線形計画法 / 権限計算 / 型推論 / プログラム言語 … More Except Principal Investigator プログラム検証 / 関数型プログラム / 型理論 / 型システム / 関数型言語 / 資源使用法解析 / 高階再帰スキーム / プログラム解析 / 高階モデル検査 / 述語制約解消 / 循環証明 / shift0/reset0 / CHC optimization / de Morgan双対性 / 不動点論理 / 関係的仕様 / 時相的仕様 / プログラム合成 / 深層学習 / 形式仕様自動抽出 / 形式的意味自動抽出 / マルウェア意味解析 / ネィティブコード / API / 記号実行 / マルウェア解析 / プライバシー / RE-DOS攻撃 / 自然言語処理 / マルウェア / バイナリコード / 命令セット / 動的記号実行 / 高階文法 / データ圧縮 / information flow analysis / concurrent programs / functional programs / type theory / program analysis / program verification / XML / プログラム変換 / 双模倣 / 割り込み / 線形最適化問題 / プログラム等価性 / デッドロック / 情報流解析 / 並行プログラム / 時間オートマトン / 実時間プログラム / 実時間性質 / 検証 / 仕様記述 / 実時間性 / プログラミング言語 / ソフトウエア学 / 時間プッシュダウンオートマトン / クロック凍結 / プッシュダウンシステム / 到達可能性解析 / 実時間システム / 形式的手法 / 並行分散システム / プロセス計算 / プログラム意味論 / 並行・分散プロセス計算 / 高階プログラム等価性証明 / 分散プロセス計算 / 計算モデル / 理論計算機科学 / 形式手法 / プログラム理論 / 並行・分散プロセス計算モデル / 環境双模倣 / ツリーオートマトン / モデル検査 / メモリ使用法解析 / 述語抽象化 / 資源使用法検証 / ソフトウェア検証 Less

Dependent refinement types and predicate constraints for program verificationPrincipal Investigator
- Principal Investigator
  
  寺内多智弘
- Project Period (FY)
  2022 – 2026
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Waseda University
Understanding malware semantics by AI-supported formal methods
- Principal Investigator
  
  小川瑞史
- Project Period (FY)
  2020 – 2025
- Research Category
  
  Grant-in-Aid for Challenging Research (Pioneering)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Japan Advanced Institute of Science and Technology
Synthesis of High-Level Programs from Temporal and Relational Specifications
- Principal Investigator
  
  海野広志
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Tohoku University
  University of Tsukuba
Program verification and program synthesis for side-channel attack resiliencePrincipal Investigator
- Principal Investigator
  
  Terauchi Tachio
- Project Period (FY)
  2018 – 2021
- Research Category
  
  Grant-in-Aid for Challenging Research (Exploratory)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Waseda University
Verification of high-level programs containing mutable higher-order recursive data structuresPrincipal Investigator
- Principal Investigator
  
  Terauchi Tachio
- Project Period (FY)
  2017 – 2021
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Waseda University
Large scale verification of higher-order programsPrincipal Investigator
- Principal Investigator
  
  Terauchi Tachio
- Project Period (FY)
  2014 – 2016
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Software
- Research Institution
  Japan Advanced Institute of Science and Technology
Verification of real-time reactive systems in high-level programming languages
- Principal Investigator
  
  Yuen Shoji
- Project Period (FY)
  2013 – 2016
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Nagoya University
Verification of Quantitative Information FlowPrincipal Investigator
- Principal Investigator
  
  TERAUCHI Tachio
- Project Period (FY)
  2011 – 2013
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Software
- Research Institution
  Nagoya University
Higher-Order Model Checking and its Applications
- Principal Investigator
  
  Kobayashi Naoki
- Project Period (FY)
  2011 – 2015
- Research Category
  
  Grant-in-Aid for Scientific Research (S)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  The University of Tokyo
  Tohoku University
Formal Verification of Higher-Order Open Systems
- Principal Investigator
  
  SUMII Eijiro
- Project Period (FY)
  2010 – 2014
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Tohoku University
Advancement and Application of Type Theory for Improving Software Safety
- Principal Investigator
  
  KOBAYASHI Naoki
- Project Period (FY)
  2008 – 2010
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  Tohoku University
Verification of Multi-thread Programs via Linear ProgrammingPrincipal Investigator
- Principal Investigator
  
  TERAUCHI Tachio
- Project Period (FY)
  2008 – 2010
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Software
- Research Institution
  Tohoku University
Type Theory for Software Safety
- Principal Investigator
  
  KOBAYSHI Naoki
- Project Period (FY)
  2005 – 2007
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Tohoku University

[Journal Article] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024
- Author(s)
  Kawamata Fuga, Unno Hiroshi, Sekiyama Taro, Terauchi Tachio
- Journal Title
  
  Proceedings of the ACM on Programming Languages (POPL)
  
  Volume: 8 Issue: POPL Pages: 115-147
- DOI
  10.1145/3633280
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H00582, KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-23K24826
[Journal Article] Trace Effects for a Language with Algebraic Effect Handlers2023
- Author(s)
  川俣楓河, 寺内多智弘
- Journal Title
  
  Computer Software
  
  Volume: 40 Issue: 2 Pages: 2_19-2_48
- DOI
  10.11309/jssst.40.2_19
- ISSN
  0289-6540
- Year and Date
  2023-04-21
- Language
  Japanese
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20K20625, KAKENHI-PROJECT-23K24826
[Journal Article] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
- Journal Title
  
  In Proceedings of the 50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023), PACMPL 7(POPL)
  
  Volume: 7 Issue: POPL Pages: 2111-2140
- DOI
  10.1145/3571265
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[Journal Article] On Lookaheads in Regular Expressions with Backreferences2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Journal Title
  
  IEICE Transactions on Information and Systems E106-D (5)
  
  Volume: 5 Pages: 959-975
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K24826
[Journal Article] On Lookaheads in Regular Expressions with Backreferences2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi.
- Journal Title
  
  IEICE Trans. Inf. & Syst.
  
  Volume: E106.D Issue: 5 Pages: 959-975
- DOI
  10.1587/transinf.2022EDP7098
- ISSN
  0916-8532, 1745-1361
- Year and Date
  2023-05-01
- Language
  English
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20K20625
[Journal Article] On Lookaheads in Regular Expressions with Backreferences2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Journal Title
  
  In Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
  
  Volume: 228
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K24826
[Journal Article] Repairing Regular Expressions for Extraction2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Journal Title
  
  In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), PACMPL 7(PLDI)
  
  Volume: 7 Issue: PLDI Pages: 1633-1656
- DOI
  10.1145/3591287
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K24826
[Journal Article] On the Expressive Power of Regular Expressions with Backreferences2023
- Author(s)
  Taisei Nogami, Tachio Terauchi
- Journal Title
  
  In Proceedings of the 48th Mathematical Foundations of Computer Science (MFCS 2023), Leibniz International Proceedings in Informatics (LIPIcs) 272
  
  Volume: LIPICS
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K24826
[Journal Article] On Lookaheads in Regular Expressions with Backreferences2022
- Author(s)
  Nariyoshi Chida、Tachio Terauchi
- Journal Title
  
  Proceedings of International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
  
  Volume: 228
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K20380
[Journal Article] Repairing DoS Vulnerability of Real-World Regexes2022
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Journal Title
  
  In Proceedings of the 43rd IEEE Symposium on Security and Privacy (S&P 2022), IEEE Computer Society
  
  Volume: S&P 2022 Pages: 2060-2077
- DOI
  10.1109/sp46214.2022.9833597
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23K24826, KAKENHI-PROJECT-23K20380
[Journal Article] Constraint-Based Relational Verification2021
- Author(s)
  Unno Hiroshi、Terauchi Tachio、Koskinen Eric
- Journal Title
  
  Proceedings of CAV 2021, Springer LNCS
  
  Volume: 12759 Pages: 742-766
- DOI
  10.1007/978-3-030-81685-8_35
- ISBN
  9783030816841, 9783030816858
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-23K20380
[Journal Article] Bucketing and information flow analysis for provable timing attack mitigation2020
- Author(s)
  Terauchi Tachio、Antonopoulos Timos
- Journal Title
  
  Journal of Computer Security
  
  Volume: 28 Issue: 6 Pages: 607-634
- DOI
  10.3233/jcs-191356
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-23K20380
[Journal Article] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020
- Author(s)
  KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
- Journal Title
  
  Computer Software
  
  Volume: 37 Issue: 1 Pages: 1_39-1_52
- DOI
  10.11309/jssst.37.1_39
- NAID
  130007815024
- ISSN
  0289-6540
- Year and Date
  2020-01-24
- Language
  Japanese
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
[Journal Article] Games for Security Under Adaptive Adversaries2019
- Author(s)
  Antonopoulos Timos, Terauchi Tachio
- Journal Title
  
  In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019)
  
  Volume: CSF 2019 Pages: 216-229
- DOI
  10.1109/csf.2019.00022
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720
[Journal Article] A Formal Analysis of Timing Channel Security via Bucketing2019
- Author(s)
  Terauchi Tachio, Antonopoulos Timos
- Journal Title
  
  In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science
  
  Volume: 11426 Pages: 29-50
- DOI
  10.1007/978-3-030-17138-4_2
- ISBN
  9783030171377, 9783030171384
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720
[Journal Article] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018
- Author(s)
  Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
- Journal Title
  
  Proceedings of LICS 2018
  
  Volume: 印刷中 Pages: 759-768
- DOI
  10.1145/3209108.3209204
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720
[Journal Article] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs2018
- Author(s)
  Hiroshi Unno, Yuki Satake, and Tachio Terauchi
- Journal Title
  
  Proceedings of the 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2018), PACMPL
  
  Volume: 2 Issue: POPL Pages: 1-29
- DOI
  10.1145/3158100
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723, KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-15H05706
[Journal Article] Compositional Synthesis of Leakage Resilient Programs2017
- Author(s)
  Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
- Journal Title
  
  Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017)
  
  Volume: 印刷中
- Peer Reviewed / Acknowledgement Compliant / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Journal Article] Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels2017
- Author(s)
  Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei
- Journal Title
  
  Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017)
  
  Volume: 印刷中
- Peer Reviewed / Acknowledgement Compliant / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Journal Article] Compositional Synthesis of Leakage Resilient Programs2017
- Author(s)
  Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 10204 Pages: 277-297
- DOI
  10.1007/978-3-662-54455-6_13
- ISBN
  9783662544549, 9783662544556
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25280023, KAKENHI-PROJECT-17H01720
[Journal Article] Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels2017
- Author(s)
  Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei
- Journal Title
  
  Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), ACM SIGPLAN Notices
  
  Volume: 52(6) Pages: 362-375
- DOI
  10.1145/3062341.3062378
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Journal Article] Temporal Verification of Higher-Order Functional Programs2016
- Author(s)
  Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
- Journal Title
  
  In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
  
  Volume: 51 (1) Pages: 57-68
- DOI
  10.1145/2837614.2837667
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-25280020, KAKENHI-PROJECT-25280023
[Journal Article] Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling2015
- Author(s)
  Hiroshi Unno, Tachio Terauchi.
- Journal Title
  
  Proceedings of TACAS 2015, LNCS
  
  Volume: 9035 Pages: 149-163
- DOI
  10.1007/978-3-662-46681-0_10
- ISBN
  9783662466803, 9783662466810
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-23220001
[Journal Article] Relaxed Stratication: A New Approach to Practical Complete Predicate Refinement2015
- Author(s)
  Tachio Terauchi, Hiroshi Unno
- Journal Title
  
  Proceedings of ESOP 2015, LNCS
  
  Volume: 9032 Pages: 610-633
- DOI
  10.1007/978-3-662-46669-8_25
- ISBN
  9783662466681, 9783662466698
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-23220001
[Journal Article] Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR2015
- Author(s)
  Tachio Terauchi
- Journal Title
  
  In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science
  
  Volume: 9291 Pages: 128-144
- DOI
  10.1007/978-3-662-48288-9_8
- ISBN
  9783662482872, 9783662482889
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-25280023
[Journal Article] Local temporal reasoning2014
- Author(s)
  Eric Koskinen, Tachio Terauchi
- Journal Title
  
  Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
  
  Volume: CSL-LICS'14 Pages: 1-10
- DOI
  10.1145/2603088.2603138
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-25280023, KAKENHI-PROJECT-26330082
[Journal Article] Automatic Termination Verification for Higher-Order Functional Programs2014
- Author(s)
  Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
- Journal Title
  
  Proceedings of ESOP 2014, LNCS
  
  Volume: 8410 Pages: 392-411
- DOI
  10.1007/978-3-642-54833-8_21
- ISBN
  9783642548321, 9783642548338
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026, KAKENHI-PROJECT-25280023, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082
[Journal Article] Automated Verification of Higher-order Functional Programs2013
- Author(s)
  Tachio Terauchi
- Journal Title
  
  Proceeings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science, Springer
  
  Volume: 7294 Pages: 2-2
- DOI
  10.1007/978-3-642-29822-6_2
- ISBN
  9783642298219, 9783642298226
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] Automating Relatively Complete Verification of Higher-Order Functional Programs. In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)2013
- Author(s)
  Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
- Journal Title
  
  ACM SIGPLAN Notices
  
  Volume: 48(1) Pages: 75-86
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて2013
- Author(s)
  岩塚卓也,寺内多智弘,結縁祥治
- Journal Title
  
  情報処理学会論文誌 : プログラミング(PRO)
  
  Volume: 6(3)
- NAID
  110009656444
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] Automating relatively complete verification of higher-order functional programs2013
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
- Journal Title
  
  Proceedings of The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13
  
  Volume: - Pages: 75-86
- DOI
  10.1145/2429069.2429081
- NAID
  120007136948
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026
[Journal Article] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて2013
- Author(s)
  岩塚卓弥, 寺内多智弘, 結縁祥治
- Journal Title
  
  情報処理学会論文誌プログラミング(PRO)
  
  Volume: 6(3) Pages: 20-32
- NAID
  110009656444
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] Quantitative Information Flow as Safety and Liveness Hyperproperties2013
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  Theoretical Computer Science
  
  Volume: - Pages: 167-182
- DOI
  10.1016/j.tcs.2013.07.031
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23700026, KAKENHI-PROJECT-26330082
[Journal Article] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて2013
- Author(s)
  岩塚卓弥、寺内多智弘、結縁祥治
- Journal Title
  
  情報処理学会論文誌(PRO)
  
  Volume: 6(3) Pages: 20-32
- NAID
  110009656444
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-25280023
[Journal Article] Quantitative Information Flow as Safety and Liveness Hyperproperties. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012)2012
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  Electronic Proceedings in Theoretical Computer Science
  
  Volume: 85 Pages: 77-91
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] Quantitative Information Flow as Safety and Liveness Hyperproperties2012
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science
  
  Volume: 85 Pages: 77-91
- DOI
  10.4204/eptcs.85.6
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] On Bounding Problems of Quantitative Information Flow2011
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  Journal of Computer Security
  
  Volume: 19.6 Pages: 1029-1082
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] On bounding problems of quantitative information flow2011
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Journal of Computer Security
  
  Volume: 19 Issue: 6 Pages: 1029-1082
- DOI
  10.3233/jcs-2011-0437
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23700026
[Journal Article] Dependent types from counterexamples2010
- Author(s)
  Tachio Terauchi
- Journal Title
  
  Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2010) 45
  
  Pages: 119-130
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Dependent Types from Counterexamples2010
- Author(s)
  Tachio Terauchi
- Journal Title
  
  In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010)
  
  Volume: ACM Pages: 119-130
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] On Bounding Problems of Quantitative Information Flow2010
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 15^<th> European Symposium on Research in Computer Security (ESORICS 2010)
  
  Volume: 6345 Pages: 357-372
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] On Bounding Problems of Quantitative Information Flow2010
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science
  
  Volume: 6345, Springer Pages: 357-372
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities2010
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society
  
  Pages: 15-27
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20240001
[Journal Article] On Bounding Problems of Quantitative Information Flow2010
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010) Lecture Notes in Computer Science
  
  Volume: 6345 Pages: 357-372
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20240001
[Journal Article] Dependent types from counterexamples2010
- Author(s)
  Tachio Terauchi
- Journal Title
  
  Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL'10) 45
  
  Pages: 119-130
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20240001
[Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities2010
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 23^<rd> IEEE Computer Security Foundations Symposium (CSF 2010)
  
  Pages: 15-27
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities2010
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society
  
  Pages: 15-27
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Polymorphic Fractional Capabilities2009
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 16th International Static Analysis Symposium(SAS 2009) 5673
  
  Pages: 36-51
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Polymorphic Fractional Capabilities2009
- Author(s)
  Hirotoshi Yasuoka and Tachio Terauchi
- Journal Title
  
  In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science
  
  Volume: 5673, Springer Pages: 36-51
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Polymorphic Fractional Capabilities2009
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Journal Title
  
  Proceedings of the 16th International Symposium on Static Analysis(SAS'09) 5673
  
  Pages: 36-51
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20240001
[Journal Article] Inferring Channel Buffer Bounds via Linear Programming2008
- Author(s)
  Tachio Terauchiand Adam Megacz
- Journal Title
  
  In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science
  
  Volume: 4960, Springer Pages: 284-298
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] A Capability Calculus for Concurrency and Determinism2008
- Author(s)
  Tachio Terauchi, Alex Aiken
- Journal Title
  
  ACM Transactions on Programming Languages and Systems (TOPLAS)
  
  Volume: 30(5)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Checking Race Freedom via Linear Programming2008
- Author(s)
  Tachio Terauchi
- Journal Title
  
  Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation(PLDI 2008)
  
  Pages: 1-10
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] A Type System for Observational Determinism2008
- Author(s)
  Tachio Terauchi
- Journal Title
  
  Proceedings of the 21st IEEE Computer Security Foundations Symposium(CSF 2008)
  
  Pages: 287-300
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Inferring Channel Buffer Bounds via Linear Programming2008
- Author(s)
  Tachio Terauchi, Adam Megacz
- Journal Title
  
  Proceedings of the 17th European Symposium on Programming(ESOP'08) 4960
  
  Pages: 284-298
- Description
  「研究成果報告書概要(和文)」より
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-17300003
[Journal Article] Inferring Channel Buffer Bounds via Linear Programming2008
- Author(s)
  Tachio Terauchi and Adam Megacz
- Journal Title
  
  Proceedings of the 17th European Symposium on Programming(ESOP'08), Springer Lecture Notes in Computer Science 4960
  
  Pages: 284-298
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-17300003
[Journal Article] Checking Race Freedom via Linear Programming2008
- Author(s)
  Tachio Terauchi
- Journal Title
  
  In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008)
  
  Volume: ACM Pages: 1-10
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] A Type System for Observational Determinism2008
- Author(s)
  Tachio Terauchi
- Journal Title
  
  In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), IEEE Computer Society
  
  Pages: 287-300
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Witnessing Side Effects2008
- Author(s)
  Tachio Terauchi, Alex Aiken
- Journal Title
  
  ACM Transactions on Programming Languages and Systems (TOPLAS)
  
  Volume: 30(3)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Journal Article] Inferring Channel Buffer Bounds via Linear Programming2008
- Author(s)
  Tachio Terauchi and Adam Megacz
- Journal Title
  
  Proceedings of the 17th European Symposium on Programming(ESOP 2008) 4960
  
  Pages: 284-298
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20700019
[Presentation] Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness2024
- Author(s)
  野上大成, 寺内多智弘
- Organizer
  ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2024
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 159: Web Application Security
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.2024
- Author(s)
  Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi
- Organizer
  51st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2024)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Repairing Regular Expressions for Extraction2024
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024
- Author(s)
  Fuga Kawamata, Taro Sekiyama, Hiroshi Unno, Tachio Terauchi
- Organizer
  ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Nested Data Type における多相再帰のための主要型付けを持つ型システム2024
- Author(s)
  川原知真, 寺内多智弘
- Organizer
  ソフトウェア科学会第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2023
- Author(s)
  Tachio Terauchi
- Organizer
  Technology Challenges in Non-Traditional Security
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2023
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 180:The Art of SAT
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Nested Data Type における多相再帰の型推論手法 (ポスター発表)2023
- Author(s)
  川原知真, 寺内多智弘
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] 代数的エフェクトハンドラのための篩型システム (ポスター発表)2023
- Author(s)
  川俣楓河, 海野広志, 関山太郎, 寺内多智弘
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  第22回情報科学技術フォーラム（FIT2023
- Invited
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023
- Author(s)
  Unno Hiroshi、Terauchi Tachio、Gu Yu、Koskinen Eric
- Organizer
  POPL 2023
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K20380
[Presentation] On Lookaheads in Regular Expressions with Backreferences2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] 後方参照付正規表現の表現力について2023
- Author(s)
  野上大成, 寺内多智弘
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2023
- Author(s)
  Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 203:Effect Handlers and General-Purpose Languages
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Applications of Program Verification and Synthesis Techniques to Security, from Non-Interference to ReDoS2023
- Author(s)
  Tachio Terauchi
- Organizer
  Vietnam-Japan Autumn School on Cyber Security
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] Repairing Regular Expressions for Extraction.2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification2023
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen
- Organizer
  50th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2023), pp.2111-2140
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] On Lookaheads in Regular Expressions with Backreferences (Poster Presentation)2023
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] 後方参照付正規表現の表現力について2023
- Author(s)
  野上大成, 寺内多智弘
- Organizer
  ソフトウェア科学会第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] On the Expressive Power of Regular Expressions with Backreferences.2023
- Author(s)
  Taisei Nogami, Tachio Terauchi
- Organizer
  48th Mathematical Foundations of Computer Science (MFCS 2023)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2022
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト2022
- Author(s)
  川俣楓河、寺内多智弘
- Organizer
  ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Repairing DoS Vulnerability of Real-World Regexes (from IEEE S&P 2022)2022
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  2022年暗号と情報セキュリティワークショップ
- Invited
- Data Source
  KAKENHI-PROJECT-23K24826
[Presentation] On Lookaheads in Regular Expressions with Backreferences2022
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), LIPICS Vol. 228, pp.15:1-15:18
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2022
- Author(s)
  Nariyoshi Chida, Tachio Terauchi
- Organizer
  43rd IEEE Symposium on Security and Privacy (S&P 2022), pp.2060-2077
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Repairing DoS Vulnerability of Real-World Regexes2022
- Author(s)
  Nariyoshi Chida and Tachio Terauchi
- Organizer
  ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト2022
- Author(s)
  川俣楓河, 寺内多智弘
- Organizer
  ソフトウェア科学会第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Constraint-based Relational Verification2021
- Author(s)
  Tachio Terauchi
- Organizer
  Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Constraint-Based Relational Verification2021
- Author(s)
  Tachio Terauchi
- Organizer
  Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Constraint-based Relational Verification2021
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Eric Koskinen
- Organizer
  33rd International Conference on Computer-Aided Verification (CAV 2021), Springer LNCS 12759, pp.742-766
- Data Source
  KAKENHI-PROJECT-20K20625
[Presentation] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019
- Author(s)
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
- Organizer
  日本ソフトウェア科学会第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2019
- Author(s)
  Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
- Organizer
  Dagstuhl Seminar 19371: Deduction Beyond Satisfiability
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] On Cut-Elimination Theorem in Cyclic-Proof Systems2019
- Author(s)
  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
- Organizer
  Third Workshop on Mathematical Logic and its Applications (MLA 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Inferring Simple Strategies for Efficient Quantified SMT Solving2019
- Author(s)
  Souta Yamauchi, Tachio Terauchi
- Organizer
  17th Asian Symposium on Programming Languages and Systems (APLAS 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] On Cut-Elimination Theorem in Cyclic-Proof Systems2019
- Author(s)
  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
- Organizer
  Third Workshop on Mathematical Logic and its Applications (MLA 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2019
- Author(s)
  Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
- Organizer
  Dagstuhl Seminar 19371: Deduction Beyond Satisfiability
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Solving First-Order Fixpoint Logic for Program Verification2019
- Author(s)
  Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
- Organizer
  Third Workshop on Mathematical Logic and its Applications (MLA 2019)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Solving First-Order Fixpoint Logic for Program Verification2019
- Author(s)
  Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
- Organizer
  Third Workshop on Mathematical Logic and its Applications (MLA 2019)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019
- Author(s)
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
- Organizer
  日本ソフトウェア科学会第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] On Cut-elimination in Cyclic Proof Systems2019
- Author(s)
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
- Organizer
  The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Inferring Simple Strategies for Efficient Quantified SMT Solving2019
- Author(s)
  Souta Yamauchi, Tachio Terauchi
- Organizer
  17th Asian Symposium on Programming Languages and Systems (APLAS 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] On Cut-elimination in Cyclic Proof Systems2018
- Author(s)
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
- Organizer
  The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Information Flow Security and its Applications to Side Channel Attack Resilience2018
- Author(s)
  Tachio Terauchi
- Organizer
  The 4th Franco-Japanese Workshop on Cybersecurity
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K19787
[Presentation] Compositional Synthesis of Leakage Resilient Programs2018
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 115: Intensional and Extensional Aspects of Computation: From Computability and Complexity to Program Analysis and Security
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] Information Flow Security and its Applications to Side Channel Attack Resilience2018
- Author(s)
  Tachio Terauchi
- Organizer
  The 4th Franco-Japanese Workshop on Cybersecurity
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17H01720
[Presentation] On Predicate Refinement Heuristics in Program Verification with CEGAR.2016
- Author(s)
  Tachio Terauchi
- Organizer
  The 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016)
- Place of Presentation
  Eindhoven, Netherlands
- Invited
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] On Predicate Refinement Heuristics in Program Verification with CEGAR2016
- Author(s)
  Tachio Terauchi
- Organizer
  The 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016)
- Place of Presentation
  Eindhoven, Netherlands
- Year and Date
  2016-04-03
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] Temporal Verification of Higher-Order Functional Programs2016
- Author(s)
  Tachio Terauchi
- Organizer
  Dagstuhl Seminar 16131: Language Based Verification Tools for Functional Programs
- Place of Presentation
  Dagstuhl, Germany
- Year and Date
  2016-03-28
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] Predicate Refinement Heuristics in Program Verification with CEGAR2015
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 063: Semantics and Verification of Object-Oriented Languages
- Place of Presentation
  NII Shonan Village Center, Hayamamachi, Japan
- Year and Date
  2015-09-21
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] Verification of Object-Oriented Programs via Refinement Types (Poster Presentation)2015
- Author(s)
  Nam Mai and Tachio Terauchi
- Organizer
  The 13th Asian Symposium on Programming Languages and Systems (APLAS 2015)
- Place of Presentation
  Pohang, Korea
- Year and Date
  2015-11-30
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] Automatic Termination Verification for Higher-Order Functional Programs2014
- Author(s)
  Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
- Organizer
  ソフトウェア科学会第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
- Place of Presentation
  熊本県阿蘇市
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automatic Termination Verification for Higher-Order Functional Programs2014
- Author(s)
  Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
- Organizer
  ソフトウェア科学会第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automatic Termination Verification for Higher-Order Functional Programs2014
- Author(s)
  Takya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
- Organizer
  ESOP 2014
- Place of Presentation
  Grenoble, France
- Data Source
  KAKENHI-PROJECT-25280023
[Presentation] Automatic Termination Verification for Higher-Order Functional Programs2014
- Author(s)
  Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
- Organizer
  The 23rd European Symposium on Programming (ESOP 2014)
- Place of Presentation
  Grenoble, France
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] 無限小定数と限量子除去法によるハイブリッドシステムの検証2013
- Author(s)
  岩塚卓也,寺内多智弘,結縁祥治
- Organizer
  情報処理学会第93回プログラミング研究会
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automating Relatively Complete Verification of Higher-Order Functional Programs2013
- Author(s)
  Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
- Organizer
  ソフトウェア科学会第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013)
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] 無限小定数と限量子除去法によるハイブリッドシステムの検証2013
- Author(s)
  岩塚卓弥, 寺内多智弘, 結縁祥治
- Organizer
  情報処理学会プログラミング研究会
- Place of Presentation
  国立情報学研究所
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automating Relatively Complete Verification of Higher-order Functional Programs2013
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
- Organizer
  日本ソフトウェア科学界第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
- Place of Presentation
  福島県会津若松東山温泉御宿東鳳
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automating Relatively Complete Verification of Higher-order Functional Programs2013
- Author(s)
  Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
- Organizer
  The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)
- Place of Presentation
  Rome, Italy
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Quantitative Information Flow as Safety and Liveness Hyperproperties2012
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Organizer
  The 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012)
- Place of Presentation
  Tallinn, Estonia
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automated Verification of Higher-order Functional Programs2012
- Author(s)
  Tachio Terauchi
- Organizer
  The 11th International Symposium on Functional and Logic Programming (FLOPS 2012)
- Place of Presentation
  神戸大学
- Invited
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] On Complexity of Verifying Quantitative Information Flow2012
- Author(s)
  Tachio Terauchi
- Organizer
  Dagstuhl Seminar 12481: Quantitative Security Analsysis
- Place of Presentation
  Dagstuhl, Germany
- Invited
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] On Complexity of Verifying Quantitative Information Flow2012
- Author(s)
  Tachio Terauchi
- Organizer
  Dagstuhl Seminar 12481 : Quantitative Security Analysis
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Automated Verification of Higher-Order Functional Programs2012
- Author(s)
  Tachio Terauchi
- Organizer
  Proceedings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science 7294
- Place of Presentation
  (pp.2. Springer)
- Invited
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Thread-based code cloning for light-weight context sensitive static race detection2011
- Author(s)
  Toshiyuki Manabe, Tachio Terauchi
- Organizer
  4th NSFC-JSPS workshop on Formal Methods
- Place of Presentation
  奈良
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Relatively Complete Type System for Higher-order Programs2011
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting on Automated Techniques for Higher-order Program Verification
- Place of Presentation
  神奈川
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Relatively Complete Refinement Types from Counterexamples2011
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 005 : Automated Techniques for Higher-Order Program Verification
- Data Source
  KAKENHI-PROJECT-23700026
[Presentation] Polymorphic Fractional Capabilities2010
- Author(s)
  Hirotoshi Yasuoka, Tachio Terauchi
- Organizer
  第12回プログラミングおよびプログラミング言語ワークショップ(PPL 2010)
- Place of Presentation
  香川県琴平
- Year and Date
  2010-03-05
- Data Source
  KAKENHI-PROJECT-20700019
[Presentation] Dependent Types from Counterexamples2010
- Author(s)
  寺内多智弘
- Organizer
  JSSST第12回プログラミングおよびプログラミング言語ワークショップ
- Place of Presentation
  香川県琴平町
- Year and Date
  2010-03-04
- Data Source
  KAKENHI-PROJECT-20700019
[Presentation] Polymorphic Fractional Capabilities2010
- Author(s)
  安岡宏俊、寺内多智弘
- Organizer
  JSSST第12回プログラミングおよびプログラミング言語ワークショップ
- Place of Presentation
  香川県琴平町
- Year and Date
  2010-03-05
- Data Source
  KAKENHI-PROJECT-20700019
[Presentation] Checking Race Freedom via Linear Programming2008
- Author(s)
  寺内多智弘
- Organizer
  JSSST第10回プログラミングおよびプログラミング言語ワークショップ
- Place of Presentation
  宮城県仙台市
- Year and Date
  2008-03-06
- Data Source
  KAKENHI-PROJECT-20700019
[Presentation] プログラム検証とインバリアント生成
- Author(s)
  寺内多智弘
- Organizer
  日本ソフトウェア科学会第31回大会
- Place of Presentation
  名古屋大学東山キャンパス・愛知県名古屋市
- Year and Date
  2014-09-07 – 2014-09-10
- Invited
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] 効率の良いLeakage Resilientプログラムの自動生成に向けて (ポスター発表)
- Author(s)
  山本真輝, 寺内多智弘
- Organizer
  日本ソフトウェア科学会第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)
- Place of Presentation
  道後プリンスホテル・愛媛県松山市
- Year and Date
  2015-03-04 – 2015-03-06
- Data Source
  KAKENHI-PROJECT-26330082
[Presentation] Information Flow Analysis and Applications to Computer Security
- Author(s)
  Tachio Terauchi
- Organizer
  NII Shonan Meeting Seminar 065: Low-level Code Analysis and Applications to Computer Security
- Place of Presentation
  湘南国際村センター・神奈川県葉山町
- Year and Date
  2015-03-01 – 2015-03-05
- Data Source
  KAKENHI-PROJECT-26330082

1. SUMII Eijiro (00333550)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
2. UNNO Hiroshi (80569575)

# of Collaborated Projects: 4 results

# of Collaborated Products: 18 results
3. KOBAYASHI Naoki (00262155)

# of Collaborated Projects: 3 results

# of Collaborated Products: 2 results
4. IGARASHI Atsushi (40323456)

# of Collaborated Projects: 3 results

# of Collaborated Products: 0 results
5. MATSUDA Kazutaka (10583627)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
6. Yuen Shoji (70230612)

# of Collaborated Projects: 1 results

# of Collaborated Products: 1 results
7. SHINOHARA Ayumi (00226151)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
8. 小川瑞史 (40362024)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
9. NGUYEN MinhLe (30509401)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
10. 関浩之 (80196948)

# of Collaborated Projects: 1 results

# of Collaborated Products: 1 results
11. 南出靖彦 (50252531)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
12. LI Guoqiang

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
13. IMAI Keigo

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
14. Ulidowski Irek

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
15. 関山太朗

# of Collaborated Projects: 0 results

# of Collaborated Products: 1 results

Terauchi Tachio 寺内 多智弘

TERAUCHI Tachio 寺内 多智弘

Research Projects

Research Products

Co-Researchers

Dependent refinement types and predicate constraints for program verificationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Understanding malware semantics by AI-supported formal methods

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Synthesis of High-Level Programs from Temporal and Relational Specifications

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Program verification and program synthesis for side-channel attack resiliencePrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Verification of high-level programs containing mutable higher-order recursive data structuresPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Large scale verification of higher-order programsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Verification of real-time reactive systems in high-level programming languages

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Verification of Quantitative Information FlowPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Higher-Order Model Checking and its Applications

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Formal Verification of Higher-Order Open Systems

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Advancement and Application of Type Theory for Improving Software Safety

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Verification of Multi-thread Programs via Linear ProgrammingPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Type Theory for Software Safety

Principal Investigator

Project Period (FY)

Terauchi Tachio 寺内多智弘

TERAUCHI Tachio 寺内多智弘