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: |
Correctness
Competition Computer science Event (computing) Tool development 020207 software engineering 0102 computer and information sciences 02 engineering and technology Mathematical proof 01 natural sciences Data science Specification languages Competition (economics) 010201 computation theory & mathematics Program verification 0202 electrical engineering electronic engineering information engineering Key (cryptography) VerifyThis State (computer science) |
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 |
Externí odkaz: |