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

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.