Large scale verification of higher-order programs

• Project/Area Number: 26330082
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Japan 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: ¥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.

Research Products

• [Journal Article] Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels (2017)
  • 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 / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Compositional Synthesis of Leakage Resilient Programs (2017)
  • 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 / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Temporal Verification of Higher-Order Functional Programs (2016)
  • 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 / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR (2015)
  • 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 / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Relaxed Stratication: A New Approach to Practical Complete Predicate Refinement (2015)
  • 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
• [Journal Article] Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling (2015)
  • 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
• [Journal Article] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 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
• [Journal Article] Local temporal reasoning (2014)
  • 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
• [Journal Article] Quantitative Information Flow as Safety and Liveness Hyperproperties (2013)
  • 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
• [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
  • Year and Date: 2016-04-03
  • Int'l Joint Research / Invited
• [Presentation] Temporal Verification of Higher-Order Functional Programs (2016)
  • 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
  • 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
  • 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
  • Int'l Joint Research
• [Presentation] Predicate Refinement Heuristics in Program Verification with CEGAR (2015)
  • 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
  • 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
• [Presentation] Information Flow Analysis and Applications to Computer Security (2015)
  • 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
• [Presentation] プログラム検証とインバリアント生成 (2014)
  • Author(s): 寺内多智弘
  • Organizer: 日本ソフトウェア科学会第31回大会
  • Place of Presentation: 名古屋大学東山キャンパス・愛知県名古屋市
  • Year and Date: 2014-09-07 – 2014-09-10
  • Invited