%0 Computer Program %A Armborst, Lukas %A Lathouwers, Sophie %A Huisman, Marieke %D 2023 %T Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation" %U %R 10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f.v1 %K Specifications %K Deductive Verification %K Annotations %K Tool interoperability %X <p>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".</p><p>hen using deductive verifiers to prove a program’s correctness, users have to write formal specifications.</p><p>Unfortunately, each tool uses its own specification language for this, which makes it difficult to reuse the specifications.</p><p>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.</p><p>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.</p><p> </p><p>This artifact allows you to reproduce the evaluation discussed in the paper.</p><p>For more information, we refer to the ReadMe inside the artifact.</p> %I 4TU.ResearchData