%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 &amp; 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>&nbsp;</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