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 *help |
¥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.
|
Report
(4 results)
Research Products
(17 results)
-
[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
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
