A certifying compiler for Java. - Christopher Colby; Peter Lee 001; George C. Necula; Fred Blau; Mark Plesko; Kenneth Cline (PLDI, 2000)