TY - DATA
T1 - Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"
PY - 2023/09/05
AU - Lukas Armborst
AU - Sophie Lathouwers
AU - Marieke Huisman
UR - 
DO - 10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f.v1
KW - Specifications
KW - Deductive Verification
KW - Annotations
KW - Tool interoperability
N2 - <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>
ER -