Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation

Lukas Armborst*, Sophie Lathouwers, Marieke Huisman

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


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.
Original languageEnglish
Title of host publicationiFM 2023
Subtitle of host publication18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings
EditorsPaula Herber, Anton Wijs
Number of pages19
ISBN (Electronic)978-3-031-47705-8
Publication statusPublished - 2024
Event18th International Conference on Integrated Formal Methods, IFM 2023 - Leiden, Netherlands
Duration: 13 Nov 202315 Nov 2023
Conference number: 18

Publication series

NameLecture notes in computer science


Conference18th International Conference on Integrated Formal Methods, IFM 2023
Abbreviated titleIFM 2023


  • NLA


Dive into the research topics of 'Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation'. Together they form a unique fingerprint.

Cite this