VerifyThis 2019: a program verification competition

Claire Dross; Carlo A. Furia; Marieke Huisman; Rosemary Monahan; Peter Müller

doi:10.1007/s10009-021-00619-x

VerifyThis 2019: a program verification competition

Claire Dross, Carlo A. Furia^*, Marieke Huisman, Rosemary Monahan, Peter Müller

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

9 Citations (Scopus)

70 Downloads (Pure)

Abstract

VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

Original language	English
Pages (from-to)	883-893
Number of pages	11
Journal	International journal on software tools for technology transfer
Volume	23
Issue number	6
Early online date	19 May 2021
DOIs	https://doi.org/10.1007/s10009-021-00619-x
Publication status	Published - Dec 2021

Keywords

Correctness proof
Functional correctness
Program verification
Verification competition

Access to Document

10.1007/s10009-021-00619-xLicence: CC BY

ArticleFinal published version, 433 KBLicence: CC BY

Cite this

@article{5d54880e17404da3b38b866640f57add,

title = "VerifyThis 2019: a program verification competition",

abstract = "VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.",

keywords = "Correctness proof, Functional correctness, Program verification, Verification competition",

author = "Claire Dross and Furia, {Carlo A.} and Marieke Huisman and Rosemary Monahan and Peter M{\"u}ller",

note = "Publisher Copyright: {\textcopyright} 2021, The Author(s).",

year = "2021",

month = dec,

doi = "10.1007/s10009-021-00619-x",

language = "English",

volume = "23",

pages = "883--893",

journal = "International journal on software tools for technology transfer",

issn = "1433-2779",

publisher = "Springer",

number = "6",

}

TY - JOUR

T1 - VerifyThis 2019

T2 - a program verification competition

AU - Dross, Claire

AU - Furia, Carlo A.

AU - Huisman, Marieke

AU - Monahan, Rosemary

AU - Müller, Peter

PY - 2021/12

Y1 - 2021/12

N2 - VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

AB - VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

KW - Correctness proof

KW - Functional correctness

KW - Program verification

KW - Verification competition

UR - http://www.scopus.com/inward/record.url?scp=85106226812&partnerID=8YFLogxK

U2 - 10.1007/s10009-021-00619-x

DO - 10.1007/s10009-021-00619-x

M3 - Article

AN - SCOPUS:85106226812

SN - 1433-2779

VL - 23

SP - 883

EP - 893

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

IS - 6

ER -

VerifyThis 2019: a program verification competition

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

VerifyThis 2019: A Program Verification Competition (Extended Report)

Cite this