VerifyThis – Verification Competition with a Human Factor

Autor: Ernst, Gidon, Huisman, Marieke, Mostowski, Wojciech, Ulbrich, Mattias, Beyer, Dirk, Kordon, Fabrice, Steffen, Bernhard
Rok vydání: 2019
Předmět:
Zdroj: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030175016
TACAS (3)
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, 176-195
STARTPAGE=176;ENDPAGE=195;TITLE=Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-17502-3_12
Popis: 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.
Databáze: OpenAIRE