Extensions and Applications of Refinement Types based on Game Semantics

• Project/Area Number: 25730035
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: University of Tsukuba
• Principal Investigator: Unno Hiroshi 筑波大学, システム情報系, 助教 (80569575)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2013: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• Keywords: プログラム検証 / 型システム / 定理自動証明 / 制約解消 / リファインメント型 / 依存型 / ホーン節制約解消 / 制約最適化 / 関係的仕様 / 帰納的定理証明 / ゲーム意味論 / トレース意味論 / 抽象解釈 / 関係的仕様検証 / 停止性検証

Outline of Final Research Achievements

The aim of this research project was to extend refinement type systems and their type checking and inference methods based on a denotational semantics, with applications to formal verification of high-level programs. The main result is the development of a fully-automated tool RCaml for path-sensitive verification of (a) termination, (b) non-termination, and (c) relational properties of high-order functional programs that manipulate algebraic data structures.

Research Products

• [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] Refinement Type Inference via Horn Constraint Optimization (2015)
  • Author(s): Kodai Hashimoto, Hiroshi Unno
  • Journal Title: Proceedings of SAS 2015, LNCS Volume: 9291 Pages: 199-216
  • DOI: 10.1007/978-3-662-48288-9_12
  • ISBN: 9783662482872, 9783662482889
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs (2015)
  • Author(s): Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
  • Journal Title: Proceedings of APLAS 2015, LNCS Volume: 9458 Pages: 295-312
  • DOI: 10.1007/978-3-319-26529-2_16
  • ISBN: 9783319265285, 9783319265292
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Verification of Tree-Processing Programs via Higher-Order Mode Checking (2015)
  • Author(s): Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
  • Journal Title: Mathematical Structures in Computer Science Volume: Volume 25, Special Issue 04 Issue: 4 Pages: 841-866
  • DOI: 10.1017/s0960129513000054
  • Peer Reviewed
• [Journal Article] Counterexample Finding and Abstraction Refinment for Automated Verification of Higher-Order Tree Transducers (2015)
  • Author(s): 松本雄磨, 小林直樹, 海野広志
  • Journal Title: Computer Software Volume: 32 Issue: 1 Pages: 1_161-1_178
  • DOI: 10.11309/jssst.32.1_161
  • NAID: 130004892316
  • ISSN: 0289-6540
  • 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] 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] Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs (2015)
  • Author(s): Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
  • Journal Title: Proceedings of CAV 2015, LNCS Volume: 未定
  • 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] 高階木変換器の自動検証のための反例発見と抽象化改良 (2014)
  • Author(s): 松本 雄磨, 小林 直樹, 海野 広志
  • Journal Title: 第 16 回プログラミングおよびプログラミング言語ワークショップ予稿集 Volume: - Pages: 1-18
  • NAID: 130004892316
  • Peer Reviewed
• [Presentation] Refinement Caml: A Refinement Type Checking and Inference Tool for OCaml (2016)
  • Author(s): Hiroshi Unno
  • Organizer: Dagstuhl Seminar on Language Based Verification Tools for Functional Programs
  • Place of Presentation: Wadern, Germany
  • Year and Date: 2016-03-31
  • Int'l Joint Research
• [Presentation] Relational Verification of Functional Programs via Induction-based Horn Constraint Solving (2016)
  • Author(s): Hiroshi Unno
  • Organizer: NII Shonan Meeting on Higher-Order Model Checking
  • Place of Presentation: 湘南国際村センター（神奈川県三浦郡）
  • Year and Date: 2016-03-19
  • Int'l Joint Research
• [Presentation] Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types (2015)
  • Author(s): Hiroshi Unno
  • Organizer: NII Shonan Meeting on Semantics and Verification of Object-Oriented Languages
  • Place of Presentation: 湘南国際村センター（神奈川県三浦郡）
  • Year and Date: 2015-09-21
  • Int'l Joint Research
• [Presentation] Automating Well-Founded Induction for Horn Clause Solving (2015)
  • Author(s): Sho Torii
  • Organizer: 日本ソフトウェア科学会第32 回大会
  • Place of Presentation: 早稲田大学（東京都新宿区）
  • Year and Date: 2015-09-11
• [Presentation] Higher-order Program Verification as Renement Type Inference (2015)
  • Author(s): Hiroshi Unno
  • Organizer: Workshop on Higher- Order Program Analysis (HOPA 2015)
  • Place of Presentation: 京都大学（京都府京都市）
  • Year and Date: 2015-07-04
  • Int'l Joint Research / Invited
• [Presentation] Automating Relatively Complete Verification of Higher-order Functional Programs (2013)
  • Author(s): 海野 広志
  • Organizer: 日本ソフトウェア科学会創設30周年記念大会
  • Place of Presentation: 東京
  • Invited
• [Remarks]
  • URL: http://www.cs.tsukuba.ac.jp/~uhiro/