Mobius Program Verification Environment

The Mobius Program Verification Environment is integrated with Eclipse. Further information can be found on the Mobius Trac. It is open source and freely available for non-commercial use.

Development of the Mobius PVE is hosted at GitHub.

Epsilon Pre-Release

The main distribution of the Epsilon Release comes in the form of an update site. Please note that all the necessary plugins are under the Mobius category.

The Mobius update site is the following: to get any last minute updates or patches to the PVE.

Please note that Z3 needs wine under linux to work, and that the feature mobius.dvcg (DirectVCGen) depends on the language C/C++ to be installed inside of eclipse.

Some of the new features and changes in the Epsilon release

  • 5 new perspectives added
  • Integration of BML
  • Additions of VCGens for use in Proof Carrying Code scenarios
  • Integration of provers: CVC3 and Z3

Third Party Update Sites

There are several plugins that are recommended for use with the Mobius PVE. These update sites and tools are the following:

Delta Release - 28 November 2008

Download the Mobius PVE delta distribution for Eclipse 3.4 on the following platforms:

New features and changes in the Delta release

  • Integrated with JML2
  • Final version of ESCJava2
See the Mobius Tools wiki for more details.

Gamma Release - 12 February 2008

Download the Mobius PVE gamma distribution for Eclipse 3.3 on the following platforms:

This PVE download includes an Eclipse distribution; just unzip the downloaded zipfile and then open Eclipse. There is a potential issue with the path+file name length on Windows XP breaching the 255 char limit depending on where the distribution file is unzipped (It unzips fine in the root but fails on, say, the user desktop).

If you already have Eclipse configured then you can use the Mobius update site:

Eclipse Workspaces

The following Eclipse workspaces are preconfigured for use with the Mobius environment:

New Mobius developers might also need to download an archive of commonly used Java tools.


Questions, suggestions and problem tickets can logged in the Mobius Trac.