KIT | KIT-Bibliothek | Impressum | Datenschutz

VerifyThis – Verification Competition with a Human Factor

Ernst, G.; Huisman, M.; Mostowski, W.; Ulbrich, M.

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.

Open Access Logo


Download
Originalveröffentlichung
DOI: 10.1007/978-3-030-17502-3_12
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Jahr 2019
Sprache Englisch
Identifikator ISBN: 978-3-030-17501-6
ISSN: 0302-9743, 1611-3349
KITopen-ID: 1000095166
Erschienen in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019; Prague; Czech Republic; 6 April 2019 through 11 April 2019. Ed.: B. Steffen
Verlag Springer, Cham
Seiten 176-195
Serie Lecture notes in computer science ; 11429
Schlagworte VerifyThis, Program verification, Specification languages, Tool development, Competition
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page