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

Large scale verification of higher-order programs

Research Project

Project/Area Number 26330082
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Software
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

Terauchi Tachio  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (70447150)

Project Period (FY) 2014-04-01 – 2017-03-31
Project Status Completed (Fiscal Year 2016)
Budget Amount *help
¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Keywordsプログラム検証 / モデル検査 / 高階関数 / 述語論理 / 型システム / 抽象詳細化 / 時相論理 / ソフトウェアモデル検査 / 時相論理仕様 / 抽象解釈 / 述語抽象 / ソフトウェア検証 / 停止性検証 / 型理論
Outline of Final Research Achievements

The goal of the research is to advance the state of the art on automatic verification techniques of higher-order functional programs. We have especially focused on the techniques based on software model checking via dependent type inference, that has gained popularity in the recent years.

The main contributions of the research are as follows: 1.) New, improved abstraction refinement methods (abstraction refinement is a technique used in software model checking), 2.) New automatic methods for verification of temporal properties (such as termination and liveness) of higher-order functional programs.

Report

(4 results)
  • 2016 Annual Research Report   Final Research Report ( PDF )
  • 2015 Research-status Report
  • 2014 Research-status Report
  • Research Products

    (17 results)

All 2017 2016 2015 2014 2013

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

  • [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: 印刷中

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

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

    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [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
    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [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
    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [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
    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [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
    • Related Report
      2014 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [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

    • Related Report
      2014 Research-status Report
    • Peer Reviewed
  • [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

    • Related Report
      2014 Research-status Report
    • Peer Reviewed
  • [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
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research / Invited
  • [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
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research / Invited
  • [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
    • Related Report
      2016 Annual Research Report
    • Invited
  • [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
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research
  • [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
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] 効率の良いLeakage Resilientプログラムの自動生成に向けて (ポスター発表)2015

    • Author(s)
      山本真輝, 寺内多智弘
    • Organizer
      日本ソフトウェア科学会 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)
    • Place of Presentation
      道後プリンスホテル・愛媛県松山市
    • Year and Date
      2015-03-04 – 2015-03-06
    • Related Report
      2014 Research-status Report
  • [Presentation] Information Flow Analysis and Applications to Computer Security2015

    • 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
    • Related Report
      2014 Research-status Report
  • [Presentation] プログラム検証とインバリアント生成2014

    • Author(s)
      寺内多智弘
    • Organizer
      日本ソフトウェア科学会第31回大会
    • Place of Presentation
      名古屋大学東山キャンパス・愛知県名古屋市
    • Year and Date
      2014-09-07 – 2014-09-10
    • Related Report
      2014 Research-status Report
    • Invited

URL: 

Published: 2014-04-04   Modified: 2018-03-22  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi