Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting Theory
| Project/Area Number |
16K00091
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 書き換えシステム / プログラム検証 |
|---|
| Outline of Final Research Achievements |
We conducted research to develop new methods for program verification based on rewriting techniques. The main results of this research are summarised as follows:
(1) Concerning rewriting systems with variable binding, we obtained several new conditions on confluence of nominal rewriting systems and other related systems. Also, we have taken part in the development of automated confluence and termination provers for versions of higher-order rewriting systems, and achieved excellent results in international competitions.
(2) Through observations on inductionless induction methods in rewriting systems without the sufficient completeness property, we developed a new verification method that is applicable to programs including those expressions which induce non-terminating computation such as infinite lists.
|
| Academic Significance and Societal Importance of the Research Achievements |
束縛変数を伴う書き換えシステムに対する合流性や停止性についての研究及びその成果は、従来の第一階項書き換えシステムに基づく帰納的定理証明手法である潜在帰納法および書き換え帰納法を、高階項に対する書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。また、十分完全性を持たない書き換えシステムにおける潜在帰納法についての研究及びその成果は、入力によって計算が停止しない様々なプログラムに対する検証手法を開発するにあたって重要になると考えられる。これらの成果を利用したプログラム及びプログラミング言語に対する検証手法は、ソフトウェアの信頼性を向上させる技術として役立つことが期待できる。
|
Report
(4 results)
Research Products
(10 results)
-
-
-
-
[Journal Article] Nominal Confluence Tool2016
Author(s)
Takahito Aoto and Kentaro Kikuchi
-
Journal Title
Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016)
Volume: 9706
Pages: 173-182
DOI
ISBN
9783319402284, 9783319402291
Related Report
Peer Reviewed / Acknowledgement Compliant
-
-
-
-
-
[Presentation] ACPH: System Description for CoCo 20162016
Author(s)
Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
Organizer
The 5th International Workshop on Confluence (IWC 2016)
Place of Presentation
Obergurgl University Center, Austria
Year and Date
2016-09-08
Related Report
Int'l Joint Research
-
