Joogie is free and open-source tool that detects infeasible code in Java programs.
Infeasible code is code that does not occur on feasible control-flow 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.
Joogie is a proof-of-concept research tool, so we apologize for any inconvenience in advance.
The current version is not user friendly. Hope to improve the user experience in future releases. Please also check the known limitations and bugs.
Detailed instructions on how to install and use the Joogie utility on your Mac are available HERE.
Joogie is a cross-platform utility capable of running on any operating system that comes with Java support (e.g. Mac OS X, Windows, Linux).
Requirements:
· Java
What's New in This Release: [ read full changelog ]
· Lots of improvements in the theorem prover interaction. Princess is now rocket fast!
· Several bug fixes that eliminate some false positives.
· There are still false positives, and those cannot be eliminated due to differences in the control-flow of source code and bytecode. Please check the README file for details.
· Added a brute force algorithm to suppress some of false positives (-sfp)
Find us on Google+
