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

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

    Publication series

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

    Conference

    ConferenceTOOLympics 2019
    CountryCzech Republic
    CityPrague
    Period6/04/197/04/19
    OtherPart of the 25th TACAS anniversary celebration

    Keywords

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

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

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