VerifyThis - Verification Competition with a Human Factor

Gidon Ernst; Marieke Huisman; Wojciech Mostowski; Mattias Ulbrich

doi:10.1007/978-3-030-17502-3_12

VerifyThis - Verification Competition with a Human Factor

Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich

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

12 Citations (Scopus)

115 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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III
Editors	Dirk Beyer, Marieke Huisman, Fabrice Kordon, Bernhard Steffen
Place of Publication	Cham
Publisher	Springer
Pages	176-195
Number of pages	20
ISBN (Electronic)	978-3-030-17502-3
ISBN (Print)	978-3-030-17501-6
DOIs	https://doi.org/10.1007/978-3-030-17502-3_12
Publication status	Published - 4 Apr 2019
Event	TOOLympics 2019 - Prague, Czech Republic Duration: 6 Apr 2019 → 7 Apr 2019

Publication series

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

Conference

Conference	TOOLympics 2019
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 7/04/19
Other	Part of the 25th TACAS anniversary celebration

Keywords

VerifyThis
Program verification
Specification languages
Tool development
Competition

Access to Document

10.1007/978-3-030-17502-3_12Licence: CC BY

ArticleFinal published version, 380 KBLicence: CC BY

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). Springer. https://doi.org/10.1007/978-3-030-17502-3_12

Ernst, Gidon ; Huisman, Marieke ; Mostowski, Wojciech et al. / 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 = apr,

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",

address = "Germany",

note = "TOOLympics 2019 ; Conference date: 06-04-2019 Through 07-04-2019",

}

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 et al.
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 proceeding › Conference contribution › Academic › peer-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

T2 - TOOLympics 2019

Y2 - 6 April 2019 through 7 April 2019

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). doi: 10.1007/978-3-030-17502-3_12

VerifyThis - Verification Competition with a Human Factor

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this