Joogie 1.0.1

Open-source utility that translates Java bytecode to Boogie
  1 Screenshot
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).

last updated on:
May 3rd, 2013, 18:14 GMT
file size:
19.7 MB
license type:
developed by:
Joogie Team
operating system(s):
Mac OS X
binary format:
Home \ Development \ Java
Download Button

In a hurry? Add it to your Download Basket!

user rating



Rate it!
What's New in version 1.0
  • 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)
read full changelog

Add your review!