• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 17H01720
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionWaseda University

Principal Investigator

Terauchi Tachio  早稲田大学, 理工学術院, 教授 (70447150)

Co-Investigator(Kenkyū-buntansha) 海野 広志  筑波大学, システム情報系, 准教授 (80569575)
Project Period (FY) 2017-04-01 – 2022-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥17,940,000 (Direct Cost: ¥13,800,000、Indirect Cost: ¥4,140,000)
Fiscal Year 2021: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2020: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2019: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2018: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2017: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Keywordsプログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 分離論理 / 循環証明 / 代数的エフェクト / ソフトウェアモデル検査 / プログラミング言語 / プログラム論理
Outline of Final Research Achievements

We have achieved the following research results. (1) New methods for temporal property verification of higher-order programs. (2) New results on cyclic proof systems,formal deduction systems for mathematical induction, and new methods for deciding validity of formulas in first-order fixpoint logic with background theories. (3) A new type and effect system for verifying temporal properties of programs with algebraic effects and handlers, an emerging programming language feature for uniformly expressing a variety of computational effects including destructive updates. (4) Research achievements on the application of program verification and synthesis techniques to security, such as a method for repairing real-world regular expressions vulnerable to ReDoS attacks. (5) New results on the formal language theory of regular expressions extended with real-world features such as backreferences and lookaheads.

Academic Significance and Societal Importance of the Research Achievements

非決定的動作を含む高階プログラムについて初の相対的完全な検証を実現するリファインメント型システムの提案、様々な問題の解決に応用できる一階不動点論理の妥当性判定のための新しいアルゴリズムを提案、深刻なセキュリティ脅威であるReDoS脆弱性を修復するため初のプログラム合成手法の提案など、本研究はこれまでのプログラミング言語・形式検証・定理証明・セキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。

Report

(6 results)
  • 2022 Final Research Report ( PDF )
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • 2018 Annual Research Report
  • 2017 Annual Research Report
  • Research Products

    (24 results)

All 2022 2021 2020 2019 2018 2017

All Journal Article (12 results) (of which Int'l Joint Research: 7 results,  Peer Reviewed: 12 results,  Open Access: 6 results,  Acknowledgement Compliant: 1 results) Presentation (12 results) (of which Int'l Joint Research: 9 results,  Invited: 5 results)

  • [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
    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [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
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [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

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Probabilistic Inference for Predicate Constraint Satisfaction2020

    • Author(s)
      Yuki Satake, Hiroshi Unno, Hinata Yanagi
    • Journal Title

      In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020)

      Volume: AAAI 2020 Pages: 1644-1651

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [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
    • Related Report
      2019 Annual Research Report 2018 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [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

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Temporal Verification of Programs via First-Order Fixpoint Logic2019

    • Author(s)
      Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
    • Journal Title

      In Proceedings of the 26th International Symposium (SAS 2019), Lecture Notes in Computer Science

      Volume: 11822 Pages: 413-436

    • DOI

      10.1007/978-3-030-32304-2_20

    • ISBN
      9783030323035, 9783030323042
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [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

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Propositional Dynamic Logic for Higher-Order Functional Programs2018

    • Author(s)
      Satake Yuki、Unno Hiroshi
    • Journal Title

      Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), Lecture Notes in Computer Science, Springer

      Volume: 10981 Pages: 105-123

    • DOI

      10.1007/978-3-319-96145-3_6

    • ISBN
      9783319961446, 9783319961453
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [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

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access
  • [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
    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [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

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Repairing DoS Vulnerability of Real-World Regexes2022

    • Author(s)
      Nariyoshi Chida, Tachio Terauchi
    • Organizer
      ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト2022

    • Author(s)
      川俣 楓河, 寺内 多智弘
    • Organizer
      ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] Constraint-Based Relational Verification2021

    • Author(s)
      Tachio Terauchi
    • Organizer
      Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research / Invited
  • [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
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research / Invited
  • [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)
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [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)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research / Invited
  • [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)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • Author(s)
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • Organizer
      日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)
    • Related Report
      2018 Annual Research Report
  • [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)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Horn Clauses and Beyond for Relational and Temporal Program Verification2018

    • Author(s)
      Hiroshi Unno
    • Organizer
      The 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Information Flow Security and its Applications to Side Channel Attack Resilience2018

    • Author(s)
      Tachio Terauchi
    • Organizer
      The 4th Franco-Japanese Workshop on Cybersecurity
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research / Invited
  • [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
    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research

URL: 

Published: 2017-04-28   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi