Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation

Lukas Armborst; Sophie Lathouwers; Marieke Huisman

doi:10.1007/978-3-031-47705-8_9

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 proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

25 Downloads (Pure)

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.

Original language	English
Title of host publication	iFM 2023
Subtitle of host publication	18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings
Editors	Paula Herber, Anton Wijs
Place of Publication	Cham
Publisher	Springer
Pages	153-171
Number of pages	19
ISBN (Electronic)	978-3-031-47705-8
ISBN (Print)	978-3-031-47704-1
DOIs	https://doi.org/10.1007/978-3-031-47705-8_9
Publication status	Published - 2024
Event	18th International Conference on Integrated Formal Methods, IFM 2023 - Leiden, Netherlands Duration: 13 Nov 2023 → 15 Nov 2023 Conference number: 18

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14300
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th International Conference on Integrated Formal Methods, IFM 2023
Abbreviated title	IFM 2023
Country/Territory	Netherlands
City	Leiden
Period	13/11/23 → 15/11/23

Keywords

2024 OA procedure

Access to Document

10.1007/978-3-031-47705-8_9

ArticleFinal published version, 279 KBLicence: Taverne

Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"
Armborst, L. (Creator), Lathouwers, S. (Creator) & Huisman, M. (Creator), 4TU.Centre for Research Data, 5 Sept 2023
DOI: 10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f, https://data.4tu.nl/datasets/21e79524-40c4-4dc1-8108-94e7b6fc6d9f
Dataset
Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation - Supplemental Material
Armborst, L. (Creator), Lathouwers, S. (Creator) & Huisman, M. (Creator), 4TU.Centre for Research Data, 18 Sept 2023
DOI: 10.4121/73361fbb-2633-4011-b615-cce19d8ac196, https://data.4tu.nl/datasets/73361fbb-2633-4011-b615-cce19d8ac196 and one more link, https://data.4tu.nl/datasets/73361fbb-2633-4011-b615-cce19d8ac196/1 (show fewer)
Dataset

Cite this

Armborst, L., Lathouwers, S., & Huisman, M. (2024). Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. In P. Herber, & A. Wijs (Eds.), iFM 2023: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings (pp. 153-171). (Lecture Notes in Computer Science; Vol. 14300). Springer. https://doi.org/10.1007/978-3-031-47705-8_9

Armborst, Lukas ; Lathouwers, Sophie ; Huisman, Marieke. / Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. iFM 2023: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. editor / Paula Herber ; Anton Wijs. Cham : Springer, 2024. pp. 153-171 (Lecture Notes in Computer Science).

@inproceedings{f53612af5ceb48bb9c0daf10e286d9da,

title = "Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation",

abstract = "Deductive verifiers can be used to prove the correctness of programs by specifying the program{\textquoteright}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.",

keywords = "2024 OA procedure",

author = "Lukas Armborst and Sophie Lathouwers and Marieke Huisman",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; 18th International Conference on Integrated Formal Methods, IFM 2023, IFM 2023 ; Conference date: 13-11-2023 Through 15-11-2023",

year = "2024",

doi = "10.1007/978-3-031-47705-8_9",

language = "English",

isbn = "978-3-031-47704-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "153--171",

editor = "Paula Herber and Anton Wijs",

booktitle = "iFM 2023",

address = "Germany",

}

Armborst, L, Lathouwers, S & Huisman, M 2024, Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. in P Herber & A Wijs (eds), iFM 2023: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14300, Springer, Cham, pp. 153-171, 18th International Conference on Integrated Formal Methods, IFM 2023, Leiden, Netherlands, 13/11/23. https://doi.org/10.1007/978-3-031-47705-8_9

Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. / Armborst, Lukas; Lathouwers, Sophie; Huisman, Marieke.
iFM 2023: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. ed. / Paula Herber; Anton Wijs. Cham: Springer, 2024. p. 153-171 (Lecture Notes in Computer Science; Vol. 14300).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation

AU - Armborst, Lukas

AU - Lathouwers, Sophie

AU - Huisman, Marieke

N1 - Conference code: 18

PY - 2024

Y1 - 2024

N2 - 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.

AB - 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.

KW - 2024 OA procedure

U2 - 10.1007/978-3-031-47705-8_9

DO - 10.1007/978-3-031-47705-8_9

M3 - Conference contribution

SN - 978-3-031-47704-1

T3 - Lecture Notes in Computer Science

SP - 153

EP - 171

BT - iFM 2023

A2 - Herber, Paula

A2 - Wijs, Anton

PB - Springer

CY - Cham

T2 - 18th International Conference on Integrated Formal Methods, IFM 2023

Y2 - 13 November 2023 through 15 November 2023

ER -

Armborst L, Lathouwers S, Huisman M. Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. In Herber P, Wijs A, editors, iFM 2023: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Cham: Springer. 2024. p. 153-171. (Lecture Notes in Computer Science). Epub 2023 Nov 6. doi: 10.1007/978-3-031-47705-8_9

Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Datasets

Specification Translator: Artifact for iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation"

Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation - Supplemental Material

Cite this