VerifyThis - Verification Competition with a Human Factor

Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich

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

6 Downloads (Pure)

Abstract

VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III
EditorsDirk Beyer, Marieke Huisman, Fabrice Kordon, Bernhard Steffen
PublisherSpringer
Pages176-195
Number of pages20
ISBN (Electronic)978-3-030-17502-3
ISBN (Print)978-3-030-17501-6
DOIs
Publication statusPublished - 4 Apr 2019
EventTOOLympics 2019 - Prague, Czech Republic
Duration: 6 Apr 20197 Apr 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Conference

ConferenceTOOLympics 2019
CountryCzech Republic
CityPrague
Period6/04/197/04/19
OtherPart of the 25th TACAS anniversary celebration

Fingerprint

Human engineering

Cite this

Ernst, G., Huisman, M., Mostowski, W., & Ulbrich, M. (2019). VerifyThis - Verification Competition with a Human Factor. In D. Beyer, M. Huisman, F. Kordon, & B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III (pp. 176-195). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-030-17502-312
Ernst, Gidon ; Huisman, Marieke ; Mostowski, Wojciech ; Ulbrich, Mattias. / VerifyThis - Verification Competition with a Human Factor. Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. editor / Dirk Beyer ; Marieke Huisman ; Fabrice Kordon ; Bernhard Steffen. Springer, 2019. pp. 176-195 (Lecture Notes in Computer Science).
@inproceedings{48c34e9722574126bee80528424e319c,
title = "VerifyThis - Verification Competition with a Human Factor",
abstract = "VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.",
author = "Gidon Ernst and Marieke Huisman and Wojciech Mostowski and Mattias Ulbrich",
year = "2019",
month = "4",
day = "4",
doi = "10.1007/978-3-030-17502-312",
language = "English",
isbn = "978-3-030-17501-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "176--195",
editor = "Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III",

}

Ernst, G, Huisman, M, Mostowski, W & Ulbrich, M 2019, VerifyThis - Verification Competition with a Human Factor. in D Beyer, M Huisman, F Kordon & B Steffen (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Lecture Notes in Computer Science, Springer, pp. 176-195, TOOLympics 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17502-312

VerifyThis - Verification Competition with a Human Factor. / Ernst, Gidon; Huisman, Marieke; Mostowski, Wojciech; Ulbrich, Mattias.

Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. ed. / Dirk Beyer; Marieke Huisman; Fabrice Kordon; Bernhard Steffen. Springer, 2019. p. 176-195 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - VerifyThis - Verification Competition with a Human Factor

AU - Ernst, Gidon

AU - Huisman, Marieke

AU - Mostowski, Wojciech

AU - Ulbrich, Mattias

PY - 2019/4/4

Y1 - 2019/4/4

N2 - VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.

AB - VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.

U2 - 10.1007/978-3-030-17502-312

DO - 10.1007/978-3-030-17502-312

M3 - Conference contribution

SN - 978-3-030-17501-6

T3 - Lecture Notes in Computer Science

SP - 176

EP - 195

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III

A2 - Beyer, Dirk

A2 - Huisman, Marieke

A2 - Kordon, Fabrice

A2 - Steffen, Bernhard

PB - Springer

ER -

Ernst G, Huisman M, Mostowski W, Ulbrich M. VerifyThis - Verification Competition with a Human Factor. In Beyer D, Huisman M, Kordon F, Steffen B, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Springer. 2019. p. 176-195. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-17502-312