Towards parallel programming environment with certified correctness and complexity

2018 Fiscal Year Final Research Report

• Project/Area Number: 15K15974
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Kyushu Institute of Technology
• Principal Investigator: Emoto Kento 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
• Project Period (FY): 2015-04-01 – 2019-03-31
• Keywords: 定理証明支援系 / 並列プログラミング

Outline of Final Research Achievements

Programs have to be correct and efficient. We have obtained the following two results for parallel programming with certified correctness and complexity: (1)
a consise notation in a proof assistant Coq for writing local complexity naively within the program code, to carry out a formal proof of its parallel complexity; and (2) a method for easy and natural manipulation of inequalities in formal proofs. These results have made it easier to build parallel programs with certified correctness and complexity.

Free Research Field

計算機科学

Academic Significance and Societal Importance of the Research Achievements

身の回りにあふれるコンピュータが安全かつ効率的に仕事をしているのは、その仕事の指示をしているプログラムが「正しく・速く」動くように作られているからである。しかし、どのような専門家であっても、人である以上、見落としなく「正しさ」と「速さ」を保証したプログラムを作ることはできない。そのため、人ではなく、見落としをしないコンピューター自身にその「正しさ」と「速さ」を保証させることが理想である。残念なことに、コンピュータにその保証をさせるにも煩雑な手順が必要であり、コストが掛かってしまう。本研究は、その手順を簡単化する手法を開発し、そのコストを下げることでより安全かつ効率的な社会の実現に貢献する。