Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation - Supplemental Material
doi: 10.4121/73361fbb-2633-4011-b615-cce19d8ac196
CC BY 4.0
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.
- 2023-09-18 first online, published, posted
- Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
DATA
- 385,310 bytesMD5:
8dded33c12610c41f00e8debb46393c4appendix.pdf -
download all files (zip)
385,310 bytes unzipped
