Specification Translator: Tool to Translate Specifications for Deductive Verifiers

doi: 10.4121/21820458.v1
The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/21820458
Datacite citation style:
Lathouwers, Sophie; Armborst, Lukas; Huisman, Marieke (2023): Specification Translator: Tool to Translate Specifications for Deductive Verifiers. Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/21820458.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite

About the Specification Translator

The Specification Translator is a tool that has been implemented as part of our research titled "Join Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". This tool will translate specifications in verified Java programs from one specification language into another. It supports the tools Krakatoa, OpenJML and VerCors.

The tool takes an annotated Java program and a target tool as input. It will then generate an annotated Java program where the annotations have been translated.

What's included in this artifact?

This artifact contains the following things:

- specification-translator.zip: A directory containing the Specification Translator tool as well as the examples used for the evaluation.

- SpecTranslatorArtifact.ova: A Virtual Machine with the Specification Translator tool, as well as the OpenJML and VerCors verifiers. It also contains the examples used for the evaluation and a script to reproduce the evaluation.

You can use the Virtual Machine to reproduce the evaluation including verification after translation.

If you just want to use the Specification Translator or have a look at the input/output files of the evaluation, then the zip file is sufficient.

License information

The Specification Translator tool is shared under the CC-BY 4.0 license.

The verifiers in the VM, as well as the examples and case studies used for the evaluation, are not licensed under the CC-BY 4.0 but under their original licenses which have been included.

  • 2023-06-19 first online, published, posted
1) ZIP file that contains Scala files, Java files, Python scripts, text files, JAR file, 2) Markdown (md) file, 3) Virtual Machine in .ova format
  • Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools


To access the source code, use the following command:

git clone https://data.4tu.nl/v3/datasets/9650e706-6335-4fdd-b669-1a72ac1fe23d.git
files (3)