The DOI displayed above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
DOI: 10.4121/73361fbb-2633-4011-b615-cce19d8ac196

Armborst, Lukas; Lathouwers, Sophie; Huisman, Marieke (2023): Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation - Supplemental Material. Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/73361fbb-2633-4011-b615-cce19d8ac196.v1

Usage statistics

Categories

• Computer Software
• Information and Computing Sciences

Keywords

Annotations Deductive Verification Specifications Tool Interoperability

Licence

CC BY 4.0

Export as...

RefWorks BibTeX Reference Manager Endnote DataCite NLM DC CFF

by Lukas Armborst , Sophie Lathouwers , Marieke Huisman

This is the appendix to the iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". Due to publisher constraints, it had to be moved online after the paper was peer-reviewed. The appendix contains the grammar for the intermediate representation used by the tool that the paper describes.

Paper abstract:

Deductive verifiers can be used to prove the correctness of programs by specifying the program's intended behaviour using annotations such as pre- and postconditions. Unfortunately, most verifiers use their own unique specification language for those contract-based annotations. While many of them have similar concepts and syntax, there are numerous semantic differences and subtleties that make it very difficult to reuse specifications between verifiers. But reusing specifications could help overcome one of the bottlenecks of deductive verification, namely writing specifications. Therefore, we present the Specification Translator, a tool to automatically translate annotations for deductive verifiers. It currently supports Java programs annotated for OpenJML, Krakatoa and VerCors. Using the Specification Translator, we show that we can reuse 81% of the annotations, which would otherwise need to be manually translated. Moreover, it allows to reuse tools such as Daikon that generate annotations only in the syntax of one specific tool.

History

• 2023-09-18 first online, published, posted

Publisher

4TU.ResearchData

Format

pdf

Funding

• Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council

Organizations

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science, Formal Methods and Tools (FMT)