Lightweight verification of array indexing
Martin Kellogg, Vlastimil Dort, Suzanne Millstein, Michael D. Ernst · 2018
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.