TY - DATA
T1 - Specification Translator: Tool to Translate Specifications for Deductive Verifiers
PY - 2023/06/19
AU - Sophie Lathouwers
AU - Lukas Armborst
AU - Marieke Huisman
UR - https://data.4tu.nl/articles/software/_/21820458
DO - 10.4121/21820458.v1
KW - Deductive verification
KW - Specifications
KW - Annotations
KW - Specification languages
KW - Semantics
KW - Translation
N2 - <p><strong>About the Specification Translator</strong></p><p>The Specification Translator is a tool that has been implemented as part of our research titled "Join Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". This tool will translate specifications in verified Java programs from one specification language into another. It supports the tools Krakatoa, OpenJML and VerCors.</p><p><br></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><br></p><p><strong>What's included in this artifact?</strong></p><p>This artifact contains the following things:</p><p>- specification-translator.zip: A directory containing the Specification Translator tool as well as the examples used for the evaluation.</p><p>- SpecTranslatorArtifact.ova: A Virtual Machine with the Specification Translator tool, as well as the OpenJML and VerCors verifiers. It also contains the examples used for the evaluation and a script to reproduce the evaluation.</p><p><br></p><p>You can use the Virtual Machine to reproduce the evaluation including verification after translation.</p><p>If you just want to use the Specification Translator or have a look at the input/output files of the evaluation, then the zip file is sufficient.</p><p><br></p><p><strong>License information</strong></p><p>The Specification Translator tool is shared under the CC-BY 4.0 license.</p><p>The verifiers in the VM, as well as the examples and case studies used for the evaluation, are <strong>not</strong> licensed under the CC-BY 4.0 but under their original licenses which have been included.</p>
ER -