Type Checking for JavaScript
JavaScript らしさを残した JavaScript のサブセット言語の型システムの話。以前読んだ論文よりちょっと前の論文。ややこしくないところは参考になりそうだけど、ややこしいところは参考にならないかも。だけど比較は必須。
author="Christopher Anderson and Paola Giannini",
title="{Type Checking for JavaScript}",
booktitle="WOOD 2004",
publisher="Elsevier",
pages="37--58",
year="2005"
Towards Automatically Eliminating Integer-Based Vulnerabilities
C プログラムの整数に関わる脆弱性を見つけて実行時に検査するコードを挿入する手法の提案。脆弱性は、ビット幅の大きい数値から小さい数値へのキャストと、符号を替えるキャストに起因する。そのため、そのようなコードを発見したら値がキャスト先の正当な値の範囲に収まっているか検査するコードを挿入する。型システムっぽい定義が出てくるけど、別にフォーマルな議論があるわけではない。
author="David Brumely and Dawn Song and Joseph Slember",
title="{Towards Automatically Eliminating Integer-Based Vulnerabilities}",
institute="Carnegie Mellon University",
year="2006"
BabyJ: From Object Based to Class Based Programming via Types
JavaScript ライクな BabyJ という言語、型情報が書ける BabyJT という言語と型システムと健全性、さらに Java ライクな言語への変換と変換の健全性などの話。個人的には incrementally add type information と書かれているのが気になったけど、具体的にどうやって incrementally add するのか書かれていなくて残念。JavaScript の型について BabyJ くらいのサブセットから始めるのはありかも。
author="Christopher Anderson and Sophia Drossopoulou",
title="{BabyJ: From Object Based to Class Based Programming via Types}",
journal="Electronic Notes in Computer Science",
volumn="82",
number="8",
pages="53--81",
year="2003"
Flow-insensitive Static Analysis for Detecting Integer Anomalies in Programs
整数オーバーフロー、アンダーフローを静的解析によって見つける手法の提案。整数式を表す抽象構文木のノード間に大小関係を表すエッジを張ったグラフを生成し、5 種類の規則に基づいて各エッジについて検証を行う。関数をまたがる解析は行わないが、MLOC クラスのソースコードもコンパイルと同程度の時間で検査できる。
author="Dipanwita Sarkar and Muthu Jagannathan and Jay Thiagarajan and Ramanathan Venkatapathy",
title="{Flow-insensitive Static Analysis for Detecting Integer Anomalies in Programs}",
institute="Microsoft Research",
year="2006"
http://research.microsoft.com/apps/pubs/default.aspx?id=70283