Joogie: Infeasible Code Detection for Java

We present Joogie, a tool that detects infeasible code in Java programs. Infeasible code is code that does not occur on feasible controlflow paths and thus has no feasible execution. Infeasible code comprises many errors detected by static analysis in modern IDEs such as guaranteed null-pointer dereference or unreachable code. Unlike existing techniques, Joogie identifies infeasible code by proving that a particular statement cannot occur on a terminating execution using techniques from static verification. Thus, Joogie is able to detect infeasible code which is overlooked by existing tools. Joogie works fully automatic, it does not require user-provided specifications and (almost) never produces false warnings.

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Stephan Arlt, Martin Schäf
• Keywords: CAV 2012, Hardware, Infeasible Code, Null Pointer Dereference, Static Analysis