Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool


A WebIDE for Overture is a VDM-SL environment that you can access if you login using a Google account. It has been developed by two Masters thesis students (Rasmus Reimer and Kasper Saaby) at Aarhus University (AU) and its backend is installed at one of the AU servers. It has functionality for managing multiple VDM-SL projects. For each project there is debugging functionality where one also can set breakpoints and inspect different things while debugging. It also supports both outline of the definitions of a model as well as proof obligation generation and browsing. It also contains a Read-Eval-Print-Loop functionality being able to make use of the different definitions and in a fast manner evaluate different expressions. Finally, it is also possible to import existing VDM-SL examples in order to easily see how one can gain value in using this tool support.


ViennaTalk logo

ViennaTalk is a VDM environment built upon Pharo Smalltalk system.

Pre-built packages for MacOSX, Linux and Windows are available at https://github.com/tomooda/ViennaTalk-doc/releases.

Demo movies

Introduction to VDM Browser ViennaTalk: Types, Values and Objects


VDMPad is a lightweight WebIDE for VDM-SL shipped with ViennaTalk.


A free VDMPad server is available by courtesy of Kyushu University, Japan. No user registration is required.


VDMTools logo

VDMTools is a fully featured toolbox for VDM-family with a long history. It has both IDE with GUI and command line tools with features including syntax checkers, type checkers, interpreters, proof obligation generators and code generators. Binary packages (for Mac, Linux and Windows) and documentation (in English and Japanese) are available at fmvdm site, and all source code and documentation are now open-sourced under GPLv3 at github repository.