Formal Modelling in VDM

5.0 Stars (3)
0 Downloads (This Week)
Last Update:


Note that VDMJ has now moved to GitHub: https://github.com/nickbattle/vdmj

VDMJ provides basic tool support for the VDM-SL, VDM++ and VDM-RT specification languages, written in Java. It includes a parser, a type checker, an interpreter (with arbitrary precision arithmetic), a debugger, a proof obligation generator and a combinatorial test generator with coverage recording, as well as JUnit support for automatic testing.

VDMJ is a command line tool, but it is used by the Overture project, which adds a graphical Eclipse IDE interface (see screen shots).

VDMJ Web Site


  • Parses, type checks, executes and debugs VDM specifications
  • Generates proof obligations
  • Generates detailed code coverage for tests in LaTeX or MS doc
  • Performs combinatorial tests
  • Supports all three VDM dialects: VDM-SL, VDM++ and VDM-RT
  • Supports plain text, LaTeX, MS doc, docx or ODF source files
  • Supports international character sets in specifications (eg. Greek, Japanese or Cyrillic)
  • Supports external libraries and remote control (tool integration)
  • Provides JUnit support for automatic testing of specifications
  • Supports arbitrary precision arithmetic


Other Useful Business Software

VoIP Monitoring without the Missing Links Icon

With global offices, wireless networks, and data traversing the Internet, troubleshooting VoIP performance is tricky.

VoIP Monitoring without the Missing Links Icon
ThousandEyes extends visibility across corporate networks as well as the public Internet, helping to solve issues from the branch through MPLS links and SIP trunks to service provider networks. Simulate pre-deployment capacity, monitor detailed performance metrics and see how QoS settings impact call quality.

User Ratings

ease 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
features 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
design 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
support 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5 0 / 5
Write a Review

User Reviews

  • 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    In the Overture project we have developed a new architecture for the VDM Abstract Syntax Tree (AST) in order to make it easier to use the platform as a basis for developing tools for formal modeling. To validate the test outputs of the parser, type checker, interpreter, proof obligation generator etc. we compare the outputs to those produced by VDMJ. VDMJ is a very mature and high quality reference and has significantly contributed to the quality of the new Overture AST archiecture.

    Posted 08/16/2013
  • 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    VDMJ is the backend of the Overture tools as the parser, typechecker, and interpreter for a variety of VDM dialects (e.g. SL, RT, ++, classic, etc). It is lean and efficient setup provides reliable accountability of VDM specifications of varied sizes. Much recommended if you want to streamline your VDM development or even integrate your own tools / code with VDM-ready features. Much recommended!!

    Posted 02/07/2013
  • 1 of 5 2 of 5 3 of 5 4 of 5 5 of 5

    VDMJ is an extremely will engineered core tool supporting the different VDM dialects in a very mature fashion. VDMJ forms the core of the Overture open source initiative (also on SF). Without VDMJ as the core of that Overture or the follow up initiatives such as DESTECS (also on SF) or COMPASS (also on SF) would not have been anywhere. I give VDMJ my warmest recommendations!

    Posted 10/27/2012
Read more reviews

Additional Project Details

Intended Audience

Developers, Quality Engineers, Architects

User Interface


Programming Language




Thanks for helping keep SourceForge clean.

Screenshot instructions:
Red Hat Linux   Ubuntu

Click URL instructions:
Right-click on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)

More information about our ad policies

Briefly describe the problem (required):

Upload screenshot of ad (required):
Select a file, or drag & drop file here.

Please provide the ad click URL, if possible:

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.

No, thanks