SoftwareApplication
name: Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"
description: Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"
description: 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.
author: https://orcid.org/0000-0001-7565-0954
author: 0000-0002-7544-447X
author: 0000-0003-4467-072X
keywords: Deductive verification
keywords: Tool interoperability
keywords: Specifications
keywords: Annotations
license:
  creative work: creativeWork
    name: CC-BY-4.0

https://orcid.org/0000-0001-7565-0954
type: Person
given name: Lukas
family name: Armborst
name: Lukas Armborst

0000-0002-7544-447X
type: Person
given name: Sophie
family name: Lathouwers
name: Sophie Lathouwers

0000-0003-4467-072X
type: Person
given name: Marieke
family name: Huisman
name: Marieke Huisman