Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

NetMeeting Default Template

Date 26 Nov 2023, 12:00 CEST
Participants PGL, LF, KP, TO, NB Minutes by NB

Review Status of the Action List

See Net Meeting Actions

No progress on issue #38 (Links to documentation repo). Carried forward.

Overture Language Board Status

RM #50 is now complete, awaiting updates to the LRM.

Currying in VDMJ will be aligned with VDMTools per previous discussions, which needs a small LRM change.

There is a new ongoing discussion about recursive measures.

Status of ViennaTalk Development

Specification slicing has been implemented on Refactoring Browser, and we are preparing for the next major release.

Status of the Overture Components


Most work on VDMJ has been in support of the QuickCheck tool, testing it with ever larger sets of specifications and improving the LSP protocol support in anticipation of GUI changes to display/interact with counterexamples. Currently, if you run QC on the command line in VSCode, any counterexamples will be highlighted in the spec as warnings; in future, we hope to be able to automatically launch execution of these counterexamples, to let the user explore why they violate a proof obligation.

A new qcrun command has been added, which allows a failed QuickCheck run to easily make a “debug” function call, using the arguments discovered in a counterexample.

VSCode Extension

No change, but Jonas Lund has joined the effort here to improve the GUI interface for proof obligations (see above).

LSP Server

See above.

Release Planning

Community Development

The web appearance of VDM

Status. We keep with the previous plan. All members are requested to open issues on improving opportunities and we as a community should also improve the pages.

Overture Traffic

See download stats on number of installs.


Workshop submission to be sent to FM Organization by mid December. LF agreed to prepare a the proposal.

Publications Status and Plans

Also see Planned Publications.

It was agreed that people should review and update this page with their planned papers.

The OVT 21 proceedings is out in arXiv. https://arxiv.org/abs/2311.07120

Any Other Business


Next year meetings suggestions:

Convener role

Hugo: It is an honour to do this role, but I have been more involved in teaching @ AU, thus less able to be on top of my community tasks. Next year, the challenge continues. With record student enrolment at AU, my workload will double, the Systems Engineering student pool will reach ~200s and the Programming Linear Algebra course I coordinate will serve ~150s students. And I have also major roles in two other massive courses at least. Thus, I think it is only fair to disclose in advance the following:

If I continue my role as Overture convener, I will be able to coordinate the calls to the core meetings and have a major role on OVT workshop organization, but I foresee less and less input from my side in the community tasks and activities.