The end of array bounds errors

Short Form


Stay in bounds: never suffer an array indexing error again, with tooling that allows you to express and enforce specifications (contracts).


A classic error that plagues programmers is an index-out-of-bounds error when trying to access an element in an array, list, or string. Typically, this causes a crash or a security vulnerability.

Up until now, the most effective way to prevent array bounds errors has been testing, coupled with extra run-time checking to detect bounds violations. This improves the robustness of your code, but there is still the possibility that your program will fail in the field.

We have built a program verification tool that guarantees that your program will never suffer an array bound exception. This tool differs from previous work in several ways. It runs at compile time, so there is no run-time overhead and is not dependent on your test suite. It is sound rather than heuristic: it gives a guarantee, in the form of a proof of correctness. It is scalable, able to quickly analyze part of your program at a time rather than doing an expensive analysis requiring the whole program. The tool is based on a theoretical foundation called dependent types.

The tool is open-source and works for the Java programming language. Although very new (it has not yet reached version 1.0), it has already detected dozens of indexing bugs in real-world programs.

We will demonstrate the tool and will explain how it works. You will leave the session with a better understanding of how to prevent bounds errors, which you can put into practice right away.

Speaking experience

Michael Ernst has given dozens of talks to tens of thousands of developers. His well-received presentations have made him a two-time JavaOne Rock Star. This is a new talk.


  • Mernst headshot

    Michael Ernst

    University of Washington


    Michael D. Ernst is a Professor in the Computer Science & Engineering department at the University of Washington.

    Ernst’s research aims to make software more reliable, more secure, and easier (and more fun!) to produce. His primary technical interests are in software engineering, programming languages, type theory, security, program analysis, bug prediction, testing, and verification. Ernst’s research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work.

    Ernst is an ACM Fellow (2014) and received the inaugural John Backus Award (2009) and the NSF CAREER Award (2002). His research has received an ICSE Most Influential Paper Award (2017), an ACM SIGSOFT Impact Paper Award (2013), 8 ACM Distinguished Paper Awards (FSE 2014, ISSTA 2014, ESEC/FSE 2011, ISSTA 2009, ESEC/FSE 2007, ICSE 2007, ICSE 2004, ESEC/FSE 2003), an ECOOP 2011 Best Paper Award, honorable mention in the 2000 ACM doctoral dissertation competition, and other honors. In 2013, Microsoft Academic Search ranked Ernst #2 in the world, in software engineering research contributions over the past 10 years. In 2016, AMiner ranked Ernst #3 among all software engineering researchers ever.

    Dr. Ernst was previously a tenured professor at MIT, and before that a researcher at Microsoft Research.

    More information is available at his homepage: