Mobius Program Verification Environment
Development of the Mobius PVE is hosted at GitHub.
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: http://www.kindsoftware.com/products/opensource/Mobius/updates/ 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:
- CheckStyle update site: http://eclipse-cs.sf.net/update/
- FindBugs update site: http://findbugs.cs.umd.edu/eclipse
- PMD update site: http://pmd.sourceforge.net/eclipse
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
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: http://www.kindsoftware.com/products/opensource/Mobius/updates/
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.