Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"

doi:10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f.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/21e79524-40c4-4dc1-8108-94e7b6fc6d9f
Datacite citation style:
Armborst, Lukas; Lathouwers, Sophie; Huisman, Marieke (2023): Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software

We present the Specification Translator, a tool that has been implemented as part of our research titled "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation".

hen using deductive verifiers to prove a program’s correctness, users have to write formal specifications.

Unfortunately, each tool uses its own specification language for this, which makes it difficult to reuse the specifications.

This tool makes this process quicker & easier by automatically translating such specifications in verified Java programs from one specification language to 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.

 

This artifact allows you to reproduce the evaluation discussed in the paper.

For more information, we refer to the ReadMe inside the artifact.

history
  • 2023-09-05 first online, published, posted
publisher
4TU.ResearchData
format
ZIP file that contains a Scala project (consisting of Scala files, Java files, a jar executable, and others) as well as related Python scripts, text files, and Debian Software Package (.deb) files for dependencies
funding
  • Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT)

DATA

files (1)