The VerifyThis Collaborative Long Term Challenge

Marieke Huisman; Raúl E. Monti; Mattias Ulbrich; Alexander Weigl

doi:10.1007/978-3-030-64354-6_10

The VerifyThis Collaborative Long Term Challenge

Marieke Huisman, Raúl E. Monti, Mattias Ulbrich, Alexander Weigl^*

^*Corresponding author for this work

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

4 Citations (Scopus)

53 Downloads (Pure)

Abstract

Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.

Original language	English
Title of host publication	Deductive Software Verification: Future Perspectives
Subtitle of host publication	Reflections on the Occasion of 20 Years of KeY
Editors	Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich
Place of Publication	Cham
Publisher	Springer
Pages	246-260
Number of pages	15
ISBN (Electronic)	978-3-030-64354-6
ISBN (Print)	978-3-030-64353-9
DOIs	https://doi.org/10.1007/978-3-030-64354-6_10
Publication status	Published - 4 Dec 2020

Publication series

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

Keywords

22/2 OA procedure

Access to Document

10.1007/978-3-030-64354-6_10

ArticleFinal published version, 285 KBLicence: Taverne

Cite this

Huisman, M., Monti, R. E., Ulbrich, M., & Weigl, A. (2020). The VerifyThis Collaborative Long Term Challenge. In W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, & M. Ulbrich (Eds.), Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY (pp. 246-260). (Lecture Notes in Computer Science; Vol. 12345). Springer. https://doi.org/10.1007/978-3-030-64354-6_10

Huisman, Marieke ; Monti, Raúl E. ; Ulbrich, Mattias et al. / The VerifyThis Collaborative Long Term Challenge. Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. editor / Wolfgang Ahrendt ; Bernhard Beckert ; Richard Bubel ; Reiner Hähnle ; Mattias Ulbrich. Cham : Springer, 2020. pp. 246-260 (Lecture Notes in Computer Science).

@inbook{5f6f89956d7a4f62abe4b4422ebabec9,

title = "The VerifyThis Collaborative Long Term Challenge",

abstract = "Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.",

keywords = "22/2 OA procedure",

author = "Marieke Huisman and Monti, {Ra{\'u}l E.} and Mattias Ulbrich and Alexander Weigl",

year = "2020",

month = dec,

day = "4",

doi = "10.1007/978-3-030-64354-6_10",

language = "English",

isbn = "978-3-030-64353-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "246--260",

editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Mattias Ulbrich",

booktitle = "Deductive Software Verification: Future Perspectives",

address = "Germany",

}

Huisman, M, Monti, RE, Ulbrich, M & Weigl, A 2020, The VerifyThis Collaborative Long Term Challenge. in W Ahrendt, B Beckert, R Bubel, R Hähnle & M Ulbrich (eds), Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. Lecture Notes in Computer Science, vol. 12345, Springer, Cham, pp. 246-260. https://doi.org/10.1007/978-3-030-64354-6_10

The VerifyThis Collaborative Long Term Challenge. / Huisman, Marieke; Monti, Raúl E.; Ulbrich, Mattias et al.
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. ed. / Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Mattias Ulbrich. Cham: Springer, 2020. p. 246-260 (Lecture Notes in Computer Science; Vol. 12345).

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

TY - CHAP

T1 - The VerifyThis Collaborative Long Term Challenge

AU - Huisman, Marieke

AU - Monti, Raúl E.

AU - Ulbrich, Mattias

AU - Weigl, Alexander

PY - 2020/12/4

Y1 - 2020/12/4

N2 - Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.

AB - Over the last years, we have seen tremendous progress in the area of deductive program verification. To demonstrate this progress, and to bring the area of deductive program verification even further, we have proposed the VerifyThis Collaborative Long Term Challenge, which calls upon the program verification community to verify different aspects of a realistic software application over a period of several months. Goal of the challenge is to foster collaboration in order to verify a realistic and industrially-relevant software application. This paper outlines the considerations that we made when selecting the challenge, and discusses how we believe it will encourage collaboration. It presents the software application that was selected for the challenge in 2019–2020, discusses the practical set up of the challenge, and briefly reports on the received solutions and an online workshop where the different solutions were presented.

KW - 22/2 OA procedure

U2 - 10.1007/978-3-030-64354-6_10

DO - 10.1007/978-3-030-64354-6_10

M3 - Chapter

SN - 978-3-030-64353-9

T3 - Lecture Notes in Computer Science

SP - 246

EP - 260

BT - Deductive Software Verification: Future Perspectives

A2 - Ahrendt, Wolfgang

A2 - Beckert, Bernhard

A2 - Bubel, Richard

A2 - Hähnle, Reiner

A2 - Ulbrich, Mattias

PB - Springer

CY - Cham

ER -

The VerifyThis Collaborative Long Term Challenge

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this