Flow Analytic Type System for Array Bound Checks
スポンサーリンク
概要
- 論文の詳細を見る
型理論のコンパイラ設計およびプログラム解析における重要性は広く認識されつつあるが,実際のコンパイラなどに適用されるには多くの問題か残されている.根本的な問題として,アセンブラ言語などの低級言語にどのような型システムが対応するか,明らかではないことがある.この問題を解決するためにはデータフロー解析と融合された型理論が必要である.1つには従来低級言語を解析するためにデータフロー解析を用いられてきたからであり,また低級言語のための型理論に関する既存研究では,明確に主張されていなくとも,本質的にはデータフロー解析を用いていると思われる研究も多く,さらにはデータフロー解析を適用することにより型理論が簡略化可能になる研究も少なくないからである.本発表ではデータフロー解析より導き出される型理論の枠組みを提案する.この枠組みにより,型理論による精密で,厳密な証明に依拠した解析,およびデータフロー解析による効率的な解析が可能となる.この枠組みを用いて配列の範囲チェックの解析のための型理論を提案する.特にコンパイラの最適化においてよく用いられながら,従来の型理論による研究では重視されてこなかったSSA形式やInduction Variableなどを型理論に組み込むことを目指す.
- 一般社団法人情報処理学会の論文
- 2003-03-15
著者
関連論文
- 東京大学におけるサーバ証明書発行体制の構築と課題
- SAX上のlazy XML treeの構成によるXSLTの最適化
- キャンパスPKIにおけるコスト構造に関する研究(マルチメディア通信,マルチメディアシステム,ライフログ活用技術、IP放送/映像伝送,一般)
- キャンパスPKIにおけるコスト構造に関する研究(マルチメディア通信,マルチメディアシステム,ライフログ活用技術、IP放送/映像伝送,一般)
- キャンパスPKIにおけるコスト構造に関する研究
- 東京大学におけるサーバ証明書発行体制の構築と課題
- An MPICH-G Network on SuperSINET and its Performance(MPI性能評価)
- マルチスレッドを利用した分散共有メモリシステムにおけるスケジューリング属性の影響
- PVMを複数ネットワーク構成に用いた通信コストの評価
- 脅威モデルの構築をもとにしたサーバ証明書発行体制の分類とその評価手法の提案(セキュリティ(1))
- レガシーWebアプリケーションに対応するPKIを用いた簡易Single Sign-Onの実現(インターネット応用及び一般)
- レガシーWebアプリケーションに対応するPKIを用いた簡易Single Sign-Onの実現(インターネット応用及び一般)
- 最適化の検証を行うコンパイラのための型システム(サイバー増大号)
- ループアンローリングに関するGNU-CのBug Fixと性能改善
- Flow Analytic Type System for Array Bound Checks
- D-9-36 キャンパスPKIのコスト構造定量化に関する検討(D-9.ライフインテリジェンスとオフィス情報システム,一般セッション)
- インライン展開を前提とした定数伝播適用ルールの提案
- ループアンローリングの特徴抽出とそのモデル化
- X86アーキテクチャのメモリ階層を考慮した最適なRegister Allocation
- A Type System for Verification of Compiler Optimizations
- メタ計算系上のコンパイラインターフェイス
- 分散共有メモリシステム上にソフトウェアによって構築されたキャッシュシステムの静的制御
- 分散環境における共有メモリ型SPMDプログラミングモデル : Split-C/PVMの実装
- 非同期通信によって自動最適化を行なう並列化コンパイラの設計
- ソーシャルブックマークにおけるタグの時系列的な依存関係の解析(ネットワーク)
- 学術機関のためのサーバ証明書発行フレームワーク(ネットワーク管理・オペレーション,若手研究者のためのフロンティア論文)
- 学術機関のためのサーバ証明書発行フレームワーク
- 侵入者の距離によりダイナミックにセキュリティレベルを制御するシステムの検討
- 侵入者の距離によりダイナミックにセキュリティレベルを制御するシステムの検討
- ライフログサービスにおけるリスクマネジメントに関する検討(ライフログと分析,グループウェアとネットワーク,ライフログ活用技術,オフィス情報システム,セキュリティ心理学とトラスト,一般)
- 並列化コンパイラにおけるプロセッサ間非同期通信命令を用いた通信コストの最適化
- ユーザインターフェイスプログラミングに見られる部分型システムのプログラミング言語への取り込み
- εDM-∈文書モデル : テキストベース、ハイパーテキストのためのモデル
- ビッグデータを活用したサービスに関するリスクアセスメント(研究速報,ビッグデータ時代を支えるセキュリティ・プライバシー保護技術論文)
- 多様なポリシーを反映可能な認証フェデレーション機構の実現(ネットワーク応用,インターネット技術とその応用論文)
- L-034 ダイナミックに制御する情報漏洩対策システムの検討(セキュリティ実装,L分野:ネットワーク・セキュリティ)
- ダイナミックなクラウド選択のためのSLAのXML化に関する提案
- ダイナミックなクラウド選択のためのSLAのXML化に関する提案
- 学割サービス実現のためのSAML-OpenIDゲートウェイの試作(認証とプライバシー,サービス管理,運用管理技術,セキュリティ管理,及び一般)
- ハイブリッド・クラウドにおける動的セキュリティ制御基盤方式
- ハイブリッド・クラウドにおける動的セキュリティ制御基盤方式
- 1503 BCPクラウド化に対する費用対効果に関する研究(一般セッション)
- ビッグデータを活用したサービスに関するリスクアセスメント
- 1106 CSIRTにおける人的資源管理方式に関する研究(一般セッション)