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

8 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
Subtitle of host publication25 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
Place of PublicationCham
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
Volume11429
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

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

Fingerprint

Human engineering

Keywords

  • VerifyThis
  • Program verification
  • Specification languages
  • Tool development
  • Competition

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; Vol. 11429). Cham: Springer. https://doi.org/10.1007/978-3-030-17502-3_12
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. Cham : 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.",
keywords = "VerifyThis, Program verification, Specification languages, Tool development, Competition",
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-3_12",
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",

}

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, vol. 11429, Springer, Cham, pp. 176-195, TOOLympics 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17502-3_12

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. Cham : Springer, 2019. p. 176-195 (Lecture Notes in Computer Science; Vol. 11429).

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.

KW - VerifyThis

KW - Program verification

KW - Specification languages

KW - Tool development

KW - Competition

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

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

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

A2 - Beyer, Dirk

A2 - Huisman, Marieke

A2 - Kordon, Fabrice

A2 - Steffen, Bernhard

PB - Springer

CY - Cham

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. Cham: Springer. 2019. p. 176-195. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-17502-3_12