Lightweight Verification of Array Indexing
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F18%3A10387151" target="_blank" >RIV/00216208:11320/18:10387151 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1145/3213846.3213849" target="_blank" >https://doi.org/10.1145/3213846.3213849</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3213846.3213849" target="_blank" >10.1145/3213846.3213849</a>
Alternative languages
Result language
angličtina
Original language name
Lightweight Verification of Array Indexing
Original language description
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 certifes, 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 verifcation 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA17-12465S" target="_blank" >GA17-12465S: Verification and Bug Hunting for Advanced Software</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
ISBN
978-1-4503-5699-2
ISSN
—
e-ISSN
neuvedeno
Number of pages
12
Pages from-to
3-14
Publisher name
ACM
Place of publication
New York, NY, USA
Event location
Amsterdam, Netherlands
Event date
Jul 16, 2018
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—