| 研究概要 |
時相論理を用いたコンパイラ最適化器の生成系を作成した.これにより,従来は実用にならないと思われていたものが手書きのものに近づいた.また,コンパイラの最適化器が正しいかどうかを,時相論理を用いて検証する方法を開発,実装した.これは,モデル検査によりバグを報告する.一方,プログラムの実行経路によって実行されない式を除去する部分冗長除去の最適化を,要求駆動の性質を用いて,ループ不変式のループ外移動を投機的に行えるように拡張した.本手法を実装し,評価した結果,従来法より効率的に高速なコードを生成できることを示した.
|
