Janota, Mikolas; Grigore, Radu; Moskal, Michal
(Association for Computing Machinery, 2007)
We devised a reachability analysis that exploits code annotations
and implemented it as a component of the extended static
checker ESC/Java2. The component reports unchecked code and a class
of errors previously undetected. ...