|
本研究では、定理証明支援系での形式証明を経た正しい（並列）プログラムの構築に対し、その支援技術の開発や具体的なモデル・言語機構の形式化を行った。形式化については、計算量を含めた低層並列計算モデル、並列計算のための負荷分散等を実現できる言語機能、並列プログラムの構成パーツ等の定式化の基礎となる recursion schemes の定理証明支援系での形式化を行った。支援技術については、これらの証明を簡単化するためのライブラリやシステムの構築を行った。これらの取り組みで得られた成果は、国際会議や国内雑誌、国内大会・研究会等で発表した。
|
