Download: PDF, slides (PDF), slides (PowerPoint), implementation.
“Lightweight verification of array indexing” by Martin Kellogg, Vlastimil Dort, Suzanne Millstein, and Michael D. Ernst. In ISSTA 2018, Proceedings of the 2018 International Symposium on Software Testing and Analysis, (Amsterdam, Netherlands), July 2018, pp. 3-14.
In languages like C, out-of-bounds array accesses lead to security vulnerabilities and crashes. Even in managed languages like Java, which check array bounds at run time, out-of-bounds accesses cause exceptions that terminate the program.
We present a lightweight type system that certifies, at compile time, that array accesses in the program are in-bounds. The type system consists of several cooperating hierarchies of dependent types, specialized to the domain of array bounds-checking. Programmers write type annotations at procedure boundaries, allowing modular verification at a cost that scales linearly with program size.
We implemented our type system for Java in a tool called the Index Checker. We evaluated the Index Checker on over 100,000 lines of open-source code and discovered array access errors even in well-tested, industrial projects such as Google Guava.
Download: PDF, slides (PDF), slides (PowerPoint), implementation.
BibTeX entry:
@inproceedings{KelloggDME2018,
author = {Martin Kellogg and Vlastimil Dort and Suzanne Millstein and
Michael D. Ernst},
title = {Lightweight verification of array indexing},
booktitle = {ISSTA 2018, Proceedings of the 2018 International
Symposium on Software Testing and Analysis},
pages = {3-14},
address = {Amsterdam, Netherlands},
month = jul,
year = {2018}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.