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

    10 Citations (Scopus)
    82 Downloads (Pure)


    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
    Number of pages20
    ISBN (Electronic)978-3-030-17502-3
    ISBN (Print)978-3-030-17501-6
    Publication statusPublished - 4 Apr 2019
    EventTOOLympics 2019 - Prague, Czech Republic
    Duration: 6 Apr 20197 Apr 2019

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceTOOLympics 2019
    Country/TerritoryCzech Republic
    OtherPart of the 25th TACAS anniversary celebration


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


    Dive into the research topics of 'VerifyThis - Verification Competition with a Human Factor'. Together they form a unique fingerprint.

    Cite this